Paul Levy

We introduce Broad Infinity, a new set-theoretic axiom scheme based on the slogan “Every time we construct a new element, we gain a new arity.” It says that three-dimensional trees whose growth is controlled by a specified class function form a set. Such trees are called broad numbers. Assuming AC (the axiom of choice) or at least the weak version known as WISC (weakly initial set of covers), we show that Broad Infinity is equivalent to Mahlo’s principle, which says that the class of all regular limit ordinals is stationary. Assuming AC or WISC, Broad Infinity also yields a convenient principle for generating a subset of a class using a “rubric” (family of rules); this directly gives the existence of Grothendieck universes, without requiring a detour via ordinals. In the absence of choice, Broad Infinity implies that the derivations of elements from a rubric form a set; this yields the existence of Tarski-style universes. Additionally, we reveal a pattern of resemblance between “wide” principles, that are provable in ZFC, and “broad” principles, that go beyond ZFC. Note: this paper uses a base theory that is weaker than ZF but includes classical first-order logic and Replacement.

We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the difficulties with traditional approaches, where divergence is bottom or where a term denotes a function from a set of environments. We see that making forcing explicit, in the manner of game semantics, allows us to avoid these problems.We begin by modelling a first-order language with sequential I/O and unbounded nondeterminism. Then we extend the model to a calculus with higher-order and recursive types, by adapting standard game semantics. Traditional adequacy proofs using logical relations are not applicable, so we use instead a novel hiding and unhiding argument

This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned.