One of the most important principles of J.-Y. Girard's Π 2 1 -logic is induction on dilators. In particular, Girard used this principle to construct his famous functor Λ. He claimed that the totality of Λ is equivalent to the set existence axiom of Π 1 1 -comprehension from reverse mathematics. While Girard provided a plausible description of a proof around 1980, it seems that the very technical details have not been worked out to this day. A few years ago, a loosely related approach led to an equivalence between Π 1 1 -comprehension and a certain Bachmann-Howard principle. The present paper closes the circle. We relate the Bachmann-Howard principle to induction on dilators. This allows us to show that Π 1 1 -comprehension is equivalent to the totality of a functor J due to P. Päppinghaus, which can be seen as a streamlined version of Λ.

We study the question of when a given countable ordinal α is Σ n 1 - or Π n 1 -reflecting in models which are neither PD models nor the constructible universe, focusing on generic extensions of L . We prove, amongst other things, that adding any number of Cohen or random reals, or forcing with Sacks forcing or any lightface Borel weakly homogeneous ccc forcing notion cannot change such reflection properties. Moreover we show that collapse forcing increases the value of the least reflecting ordinals but, curiously, to ordinals which are still smaller than the ω 1 of L .

Das, van der Giessen, and Marin recently introduced \(\mathsf{IGL}\) , an intuitionistic version of Gödel-Löb logic. Their proof systems involves ill-founded proofs with a progressiveness condition. Their completeness proof uses the principle of \(\Sigma^{1}_{1}\) -determinacy; which is not provable in \(\mathsf{ZFC}\) . We define a cyclic proof system for \(\mathsf{IGL}\) and give a proof of its completeness theorem avoiding \(\Sigma^{1}_{1}\) -determinacy.

It is shown that Holliday’s propositional Fundamental Logic is decidable in polynomial time and that first-order Fundamental Logic is decidable in double-exponential time. The proof also yields a double-exponential–time decision procedure for first-order orthologic.

We prove the following Löwenheim-Skolem theorems for first-order Gödel logic: For the Gödel logic G[0,1], a sentence ϕ has models of every infinite cardinality if and only if it has a model of cardinality ℶω(=sup⁡{ℵ0,2ℵ0,…}). For an arbitrary Gödel logic GT, a sentence ϕ has models of every infinite cardinality if and only if it has a model of cardinality ℶω1.

We prove a number of results on the determinacy of σ-projective sets of reals, i.e., those belonging to the smallest pointclass containing the open sets and closed under complements, countable unions, and projections. We first prove the equivalence between σ-projective determinacy and the determinacy of certain classes of games of variable length

Abstract For every countable wellordering $\alpha $ greater than $\omega $ , it is shown that clopen determinacy for games of length $\alpha $ with moves in $\mathbb {N}$ is equivalent to determinacy for a class of shorter games, but with more complicated payoff. In particular, it is shown that clopen determinacy for games of length $\omega ^2$ is equivalent to $\sigma $ -projective determinacy for games of length $\omega $ and that clopen determinacy for games of length $\omega ^3$ is equivalent to determinacy for games of length $\omega ^2$ in the smallest $\sigma $ -algebra on $\mathbb {R}$ containing all open sets and closed under the real game quantifier.

Abstract Extending Aanderaa’s classical result that $\pi ^{1}_{1} < \sigma ^{1}_{1}$ , we determine the order between any two patterns of iterated $\Sigma ^{1}_{1}$ - and $\Pi ^{1}_{1}$ -reflection on ordinals. We show that this order of linear reflection is a prewellordering of length $\omega ^{\omega }$ . This requires considering the relationship between linear and some non-linear reflection patterns, such as $\sigma \wedge \pi $ , the pattern of simultaneous $\Sigma ^{1}_{1}$ - and $\Pi ^{1}_{1}$ -reflection. The proofs involve linking the lengths of $\alpha $ -recursive wellorderings to various forms of stability and reflection properties satisfied by ordinals $\alpha $ within standard and non-standard models of set theory.

Abstract It is shown that the determinacy of $G_{\delta \sigma }$ games of length $\omega ^2$ is equivalent to the existence of a transitive model of ${\mathsf {KP}} + {\mathsf {AD}} + \Pi _1\textrm {-MI}_{\mathbb {R}}$ containing $\mathbb {R}$ . Here, $\Pi _1\textrm {-MI}_{\mathbb {R}}$ is the axiom asserting that every monotone $\Pi _1$ operator on the real numbers has an inductive fixpoint.

Abstract Feedback is oracle computability when the oracle consists exactly of the con- and divergence information about computability relative to that same oracle. Here we study two possible feedback hyperjumps and characterize each of them as the complete $\varSigma _1$ set relative to a level of Gödel’s constructible hierarchy $L$.

Abstract We characterize the determinacy of $F_\sigma $ games of length $\omega ^2$ in terms of determinacy assertions for short games. Specifically, we show that $F_\sigma $ games of length $\omega ^2$ are determined if, and only if, there is a transitive model of ${\mathsf {KP}}+{\mathsf {AD}}$ containing $\mathbb {R}$ and reflecting $\Pi _1$ facts about the next admissible set. As a consequence, one obtains that, over the base theory ${\mathsf {KP}} + {\mathsf {DC}} + ``\mathbb {R}$ exists,” determinacy for $F_\sigma $ games of length $\omega ^2$ is stronger than ${\mathsf {AD}}$ , but weaker than ${\mathsf {AD}} + \Sigma _1$ -separation.

Abstract We determine the consistency strength of determinacy for projective games of length ω2. Our main theorem is that $\Pi _{n + 1}^1 $ -determinacy for games of length ω2 implies the existence of a model of set theory with ω + n Woodin cardinals. In a first step, we show that this hypothesis implies that there is a countable set of reals A such that Mn (A), the canonical inner model for n Woodin cardinals constructed over A, satisfies $$A = R$$ and the Axiom of Determinacy. Then we argue how to obtain a model with ω + n Woodin cardinal from this. We also show how the proof can be adapted to investigate the consistency strength of determinacy for games of length ω2 with payoff in $^R R\Pi _1^1 $ or with σ-projective payoff.

Abstract We give examples of calculi that extend Gentzen’s sequent calculusLKby unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter thanLK-proofs.

Abstract Given a scattered space $\mathfrak{X} = \left( {X,\tau } \right)$ and an ordinal λ, we define a topology $\tau _{ + \lambda } $ in such a way that τ+0 = τ and, when $\mathfrak{X}$ is an ordinal with the initial segment topology, the resulting sequence {τ+λ}λ∈Ord coincides with the family of topologies $\left\{ {\mathcal{I}_\lambda } \right\}_{\lambda \in Ord} $ used by Icard, Joosten, and the second author to provide semantics for polymodal provability logics. We prove that given any scattered space $\mathfrak{X}$ of large-enough rank and any ordinal λ > 0, GL is strongly complete for τ+λ. The special case where $\mathfrak{X} = \omega ^\omega + 1$ and λ = 1 yields a strengthening of a theorem of Abashidze and Blass.

Gödel logics are an important class of intermediate logics with connections to many areas and applications of logic such as temporal logic, Heyting algebras, fuzzy logic, and parallel processing. In this paper, we present ten open problems in the proof and model theories of Gödel Logic. The problems can be seen to be ordered both thematically and by generality. Some of the problems have been open for more than thirty years. The second author discussed many of them with Franco Montagna, to whose memory this paper is dedicated.