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.

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.

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.

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.

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”.

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}$

For any subset $Z \subseteq {\mathbb {Q}}$, consider the set $S_Z$ of subfields $L\subseteq {\overline {\mathbb {Q}}}$ which contain a co-infinite subset $C \subseteq L$ that is universally definable in L such that $C \cap {\mathbb {Q}}=Z$. Placing a natural topology on the set ${\operatorname {Sub}({\overline {\mathbb {Q}}})}$ of subfields of ${\overline {\mathbb {Q}}}$, we show that if Z is not thin in ${\mathbb {Q}}$, then $S_Z$ is meager in ${\operatorname {Sub}({\overline {\mathbb {Q}}})}$. Here, thin and meager both mean “small”, in terms of arithmetic geometry and topology, respectively. For example, this implies that only a meager set of fields L have the property that the ring of algebraic integers $\mathcal {O}_L$ is universally definable in L. The main tools are Hilbert’s Irreducibility Theorem and a new normal form theorem for existential definitions. The normal form theorem, which may be of independent interest, says roughly that every $\exists $-definable subset of an algebraic extension of ${\mathbb Q}$ is a finite union of single points and projections of hypersurfaces defined by absolutely irreducible polynomials.

We give a systematic technical exposition of the foundations of the theory of computably compact metric spaces. We discover several new characterizations of computable compactness and apply these characterizations to prove new results in computable analysis and effective topology. We also apply the technique of computable compactness to give new and less combinatorially involved proofs of known results from the literature. Some of these results do not have computable compactness or compact spaces in their statements, and thus these applications are not necessarily direct or expected.

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

When classes of structures are not first-order definable, we might still try to find a nice description. There are two common ways for doing this. One is to expand the language, leading to notions of pseudo-elementary classes, and the other is to allow infinite conjuncts and disjuncts. In this paper we examine the intersection. Namely, we address the question: Which classes of structures are both pseudo-elementary and ${\mathcal {L}}_{\omega _1, \omega }$ -elementary? We find that these are exactly the classes that can be defined by an infinitary formula that has no infinitary disjunctions.

Elementary first-order theories of trees allowing at most, exactly $\mathrm{m}$, and any finite number of immediate descendants are introduced and proved mutually interpretable among themselves and with Robinson arithmetic, Adjunctive Set Theory with Extensionality and other well-known weak theories of numbers, sets, and strings.

We show that the weakest versions of Foreman’s minimal generic hugeness axioms cannot hold simultaneously on adjacent cardinals. Moreover, conventional forcing techniques cannot produce a model of one of these axioms.

Currently the two popular ways to practice Robinson’s nonstandard analysis are the model-theoretic approach and the axiomatic/syntactic approach. It is sometimes claimed that the internal axiomatic approach is unable to handle constructions relying on external sets. We show that internal frameworks provide successful accounts of nonstandard hulls and Loeb measures. The basic fact this work relies on is that the ultrapower of the standard universe by a standard ultrafilter is naturally isomorphic to a subuniverse of the internal universe.

We answer some questions about graphs that are reducts of countable models of Anti-Foundation, obtained by considering the binary relation of double-membership $x\in y\in x$ . We show that there are continuum-many such graphs, and study their connected components. We describe their complete theories and prove that each has continuum-many countable models, some of which are not reducts of models of Anti-Foundation.

There seems to be a view that intuitionists not only take the Axiom of Choice (AC) to be true, but also believe it a consequence of their fundamental posits. Widespread or not, this view is largely mistaken. This article offers a brief, yet comprehensive, overview of the status of AC in various intuitionistic and constructivist systems. The survey makes it clear that the Axiom of Choice fails to be a theorem in most contexts and is even outright false in some important contexts. Of the systems surveyed, only intensional type theory renders AC a theorem, but the extent of AC in that theory does not include, for instance, real analysis. Only a small amount of extensionality is required in order for the obvious proof an intuitionist might offer for AC to break down.

Suppose that we have a method which estimates the conditional probabilities of some unknown stochastic source and we use it to guess which of the outcomes will happen. We want to make a correct guess as often as it is possible. What estimators are good for this? In this work, we consider estimators given by a familiar notion of universal coding for stationary ergodic measures, while working in the framework of algorithmic randomness, i.e., we are particularly interested in prediction of Martin-Löf random points. We outline the general theory and exhibit some counterexamples. Completing a result of Ryabko from 2009 we also show that universal probability measure in the sense of universal coding induces a universal predictor in the prequential sense. Surprisingly, this implication holds true provided the universal measure does not ascribe too low conditional probabilities to individual symbols. As an example, we show that the Prediction by Partial Matching (PPM) measure satisfies this requirement with a large reserve.

The complete characterisation of order types of non-standard models of Peano arithmetic and its extensions is a famous open problem. In this paper, we consider subtheories of Peano arithmetic (both with and without induction), in particular, theories formulated in proper fragments of the full language of arithmetic. We study the order types of their non-standard models and separate all considered theories via their possible order types. We compare the theories with and without induction and observe that the theories without induction tend to have an algebraic character that allows model constructions by closing a model under the relevant algebraic operations.

Theorems of hyperarithmetic analysis (THAs) occupy an unusual neighborhood in the realms of reverse mathematics and recursion-theoretic complexity. They lie above all the fixed (recursive) iterations of the Turing jump but below ATR $_{0}$ (and so $\Pi _{1}^{1}$ -CA $_{0}$ or the hyperjump). There is a long history of proof-theoretic principles which are THAs. Until the papers reported on in this communication, there was only one mathematical example. Barnes, Goh, and Shore [1] analyze an array of ubiquity theorems in graph theory descended from Halin’s [9] work on rays in graphs. They seem to be typical applications of ACA $_{0}$ but are actually THAs. These results answer Question 30 of Montalbán’s Open Questions in Reverse Mathematics [19] and supply several other natural principles of different and unusual levels of complexity.

This work led in [25] to a new neighborhood of the reverse mathematical zoo: almost theorems of hyperarithmetic analysis (ATHAs). When combined with ACA $_{0}$ they are THAs but on their own are very weak. Denizens both mathematical and logical are provided. Generalizations of several conservativity classes ( $\Pi _{1}^{1}$ , r- $\Pi _{1}^{1}$ , and Tanaka) are defined and these ATHAs as well as many other principles are shown to be conservative over RCA $_{0}$ in all these senses and weak in other recursion-theoretic ways as well. These results answer a question raised by Hirschfeldt and reported in [19] by providing a long list of pairs of principles one of which is very weak over RCA $_{0}$ but over ACA $_{0}$ is equivalent to the other which may be strong (THA) or very strong going up a standard hierarchy and at the end being stronger than full second-order arithmetic.

Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum’s Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko’s Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment relation over a single-conclusion one.