We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on $\mathsf {IKP}$ and $\mathsf {CZF}$. Most previously studied large set axioms, notably, the constructive analogues of large cardinals below $0^\sharp $, have proof-theoretic strength weaker than full Second-Order Arithmetic. On the other hand, the situation is dramatically different for those defined via elementary embeddings. We show that by adding to $\mathsf {IKP}$ the basic properties of an elementary embedding $j\colon V\to M$ for $\Delta _0$-formulas, which we will denote by $\Delta _0\text {-}\mathsf {BTEE}_M$, we obtain the consistency of $\mathsf {ZFC}$ and more. We will also see that the consistency strength of a Reinhardt set exceeds that of $\mathsf {ZF+WA}$. Furthermore, we will define super Reinhardt sets and $\mathsf {TR}$, which is a constructive analogue of V being totally Reinhardt, and prove that their proof-theoretic strength exceeds that of $\mathsf {ZF}$ with choiceless large cardinals.

Goodstein’s principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to diverge, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we provide a self-contained and modern analysis of Goodstein’s principle, obtaining some variations and improvements. We explore notions of optimality for notation systems and apply them to the classical Goodstein process and to a weaker variant based on multiplication rather than exponentiation. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein’s result. We moreover show that by varying the initial base of the Goodstein process, one readily obtains independence results for each of the fragments $\mathsf {I}\Sigma _n$ of Peano arithmetic.

Club guessing principles were introduced by Shelah as a weakening of Jensen’s diamond. Most spectacularly, they were used to prove Shelah’s $\textsf{ZFC}$ bound on $2^{\aleph _\omega }$. These principles have found many other applications: in cardinal arithmetic and PCF theory; in the construction of combinatorial objects on uncountable cardinals such as Jónsson algebras, strong colourings, Souslin trees, and pathological graphs; to the non-existence of universals in model theory; to the non-existence of forcing axioms at higher uncountable cardinals; and many more.

In this paper, the first part of a series, we survey various forms of club guessing that have appeared in the literature, and then systematically study the various ways in which a club guessing sequence can be improved, especially in the way the frequency of guessing is calibrated.

We include an expository section intended for those unfamiliar with club guessing and which can be read independently of the rest of the article.

We show that the universal theory of the hyperfinite II$_1$ factor is not computable. The proof uses the recent result that MIP*=RE. Combined with an earlier observation of the authors, this yields a proof that the Connes Embedding Problem has a negative solution that avoids the equivalences with Kirchberg’s QWEP Conjecture and Tsirelson’s Problem.

Cook and Reckhow [5] pointed out that $\mathcal {N}\mathcal {P} \neq co\mathcal {N}\mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows:

• • There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $\mathcal {N}\mathcal {P}$ sets.

$\bigvee $

$\bigvee $

$\mathcal {N}\mathcal {P}$

$\mathcal {N}\mathcal {P}$

We study the effective versions of several notions related to incompleteness, undecidability, and inseparability along the lines of Pour-El’s insights. Firstly, we strengthen Pour-El’s theorem on the equivalence between effective essential incompleteness and effective inseparability. Secondly, we compare the notions obtained by restricting that of effective essential incompleteness to intensional finite extensions and extensional finite extensions. Finally, we study the combination of effectiveness and hereditariness, and prove an adapted version of Pour-El’s result for this combination.

We present the true stages machinery and illustrate its applications to descriptive set theory. We use this machinery to provide new proofs of the Hausdorff–Kuratowski and Wadge theorems on the structure of $\mathbf {\Delta }^0_\xi $, Louveau and Saint Raymond’s separation theorem, and Louveau’s separation theorem.

We give a short proof of a theorem of Beleznay asserting that the set $L2$ of reals coding linear orders of the form $I + I$ is complete analytic.

Due to Gödel’s incompleteness results, the categoricity of a sufficiently rich mathematical theory and the semantic completeness of its underlying logic are two mutually exclusive ideals. For first- and second-order logics we obtain one of them with the cost of losing the other. In addition, in both these logics the rules of deduction for their quantifiers are non-categorical. In this paper I examine two recent arguments—Warren [43] and Murzi and Topey [30]—for the idea that the natural deduction rules for the first-order universal quantifier are categorical, i.e., they uniquely determine its semantic intended meaning. Both of them make use of McGee’s open-endedness requirement and the second one uses in addition Garson’s [19] local models for defining the validity of these rules. I argue that the success of both these arguments is relative to their semantic or infinitary assumptions, which could be easily discharged if the introduction rule for the universal quantifier is taken to be an infinitary rule, i.e., non-compact. Consequently, I reconsider the use of the $\omega $-rule and I show that the addition of the $\omega $-rule to the standard formalizations of first-order logic is categorical. In addition, I argue that the open-endedness requirement does not make the first-order Peano Arithmetic categorical and I advance an argument for its categoricity based on the inferential conservativity requirement.

We give a simple proof that the first-order theory of well orders is axiomatized by transfinite induction, and that it is decidable.

On the basis of Poincaré and Weyl’s view of predicativity as invariance, we develop an extensive framework for predicative, type-free first-order set theory in which $\Gamma _0$ and much bigger ordinals can be defined as von Neumann ordinals. This refutes the accepted view of $\Gamma _0$ as the “limit of predicativity”.

Continuous functions on the unit interval are relatively tame from the logical and computational point of view. A similar behaviour is exhibited by continuous functions on compact metric spaces equipped with a countable dense subset. It is then a natural question what happens if we omit the latter ‘extra data’, i.e., work with ‘unrepresented’ compact metric spaces. In this paper, we study basic third-order statements about continuous functions on such unrepresented compact metric spaces in Kohlenbach’s higher-order Reverse Mathematics. We establish that some (very specific) statements are classified in the (second-order) Big Five of Reverse Mathematics, while most variations/generalisations are not provable from the latter, and much stronger systems. Thus, continuous functions on unrepresented metric spaces are ‘wild’, though ‘more tame’ than (slightly) discontinuous functions on the reals.

Traditionally, the role of general topology in model theory has been mainly limited to the study of compacta that arise in first-order logic. In this context, the topology tends to be so trivial that it turns into combinatorics, motivating a widespread approach that focuses on the combinatorial component while usually hiding the topological one. This popular combinatorial approach to model theory has proved to be so useful that it has become rare to see more advanced topology in model-theoretic articles. Prof. Franklin D. Tall has led the re-introduction of general topology as a valuable tool to push the boundaries of model theory. Most of this thesis is directly influenced by and builds on this idea.

The first part of the thesis will answer a problem of T. Gowers on the undefinability of pathological Banach spaces such as Tsirelson space. The topological content of this chapter is centred around Grothendieck spaces.

In a similar spirit, the second part will show a new connection between the notion of metastability introduced by T. Tao and the topological concept of pseudocompactness. We shall make use of this connection to show a result of X. Caicedo, E. Dueñez, J. Iovino in a much simplified manner.

The third part of the thesis will carry a higher set-theoretic content as we shall use forcing and descriptive set theory to show that the well-known theorem of M. Morley on the trichotomy concerning the number of models of a first-order countable theory is undecidable if one considers second-order countable theories instead.

The only part that did not originate from model-theoretic questions will be the fourth one. We show that $\operatorname {ZF} + \operatorname {DC} +$“all Turing invariant sets of reals have the perfect set property” implies that all sets of reals have the perfect set property. We also show that this result generalizes to all countable analytic equivalence relations. This result provides evidence in favour of a long-standing conjecture asking whether Turing determinacy implies the axiom of determinacy.

Abstract prepared by Clovis Hamel

E-mail: [email protected]

The one-variable fragment of a first-order logic may be viewed as an “S5-like” modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given in this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property.

We answer a question of Woodin [3] by showing that “$\mathrm {NS}_{\omega _1}$ is $\omega _1$-dense” holds in a stationary set preserving extension of any universe with a cardinal $\kappa $ which is a limit of ${<}\kappa $-supercompact cardinals. We introduce a new forcing axiom $\mathrm {Q}$-Maximum, prove it consistent from a supercompact limit of supercompact cardinals, and show that it implies the version of Woodin’s $(*)$-axiom for $\mathbb Q_{\mathrm {max}}$. It follows that $\mathrm {Q}$-Maximum implies “$\mathrm {NS}_{\omega _1}$ is $\omega _1$-dense.” Along the way we produce a number of other new instances of Asperó–Schindler’s $\mathrm {MM}^{++}\Rightarrow (*)$ (see [1]).

To force $\mathrm {Q}$-Maximum, we develop a method which allows for iterating $\omega _1$-preserving forcings which may destroy stationary sets, without collapsing $\omega _1$. We isolate a new regularity property for $\omega _1$-preserving forcings called respectfulness which lies at the heart of the resulting iteration theorem.

In the second part, we show that the $\kappa $-mantle, i.e., the intersection of all grounds which extend to V via forcing of size ${<}\kappa $, may fail to be a model of $\mathrm {AC}$ for various types of $\kappa $. Most importantly, it can be arranged that $\kappa $ is a Mahlo cardinal. This answers a question of Usuba [2].

Abstract prepared by Andreas Lietz

E-mail: [email protected].

URL: https://andreas-lietz.github.io/resources/PDFs/AJourneyGuidedByThe Stars.pdf.