Second order theories with ordinals and elementary comprehension

We study elementary second order extensions of the theoryID ₁ of non-iterated inductive definitions and the theoryPA _Ω of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plusΠ ₁ ¹ comprehension and bar induction without set parameters. Research supported by the Swiss National Science Foundation     

Proof and refutation in MALL as a game

We present a setting in which the search for a proof of B or a refutation of B (i.e., a proof of ¬B) can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving B or proving ¬B as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to a refutation of the formula. The game is described for multiplicative and additive linear logic (MALL). A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win (that is, neither B nor ¬B might be provable).     

Proof-theoretic conservations of weak weak intuitionistic constructive set theories

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms.     

A constructive investigation of satisfiability

We present a constructive analysis of the logical notions of satisfiability and consistency for first-order intuitionistic formulae. In particular, we use formal topology theory to provide a positive semantics for satisfiability. Then we propose a “co-inductive” logical calculus, which captures the positive content of consistency.     

The eskolemization of universal quantifiers

This paper is a sequel to the papers Baaz and Iemhoff (2006, 2009) [4] and [6] in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory of equality and the intuitionistic theory of monadic predicates.     

Order-enriched categorical models of the classical sequent calculus

It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.     

The distribution of ITRM-recognizable reals

Infinite Time Register Machines (ITRM's) are a well-established machine model for infinitary computations. Their computational strength relative to oracles is understood, see e.g. ,  and . We consider the notion of recognizability, which was first formulated for Infinite Time Turing Machines in [6] and applied to ITRM's in [3]. A real x is ITRM-recognizable iff there is an ITRM-program P   such that P^y$P^y$ stops with output 1 iff y=x$y=x$, and otherwise stops with output 0. In [3], it is shown that the recognizable reals are not contained in the ITRM-computable reals. Here, we investigate in detail how the ITRM  -recognizable reals are distributed along the canonical well-ordering _<L${<}_L$ of Gödel's constructible hierarchy L  . In particular, we prove that the recognizable reals have gaps in _<L${<}_L$, that there is no universal ITRM in terms of recognizability and consider a relativized notion of recognizability.     

Generics for computable Mathias forcing

We study the complexity of generic reals for computable Mathias forcing in the context of computability theory. The n-generics and weak n-generics form a strict hierarchy under Turing reducibility, as in the case of Cohen forcing. We analyze the complexity of the Mathias forcing relation, and show that if G is any n  -generic with n≥2$n\ge 2$ then it satisfies the jump property G⁽ⁿ⁻¹⁾_≡TG^′⊕∅⁽ⁿ⁾$G^{(n-1)}{\equiv }_T{G}^{\prime }\oplus {\varnothing }^{(n)}$. We prove that every such G has generalized high Turing degree, and so cannot have even Cohen 1-generic degree. On the other hand, we show that every Mathias n-generic real computes a Cohen n-generic real.     

A model of Cummings and Foreman revisited

This paper concerns the model of Cummings and Foreman where from ω   supercompact cardinals they obtain the tree property at each _ℵn${\mathrm{\aleph }}_n$ for 2≤n<ω$2\le n<\omega$. We prove some structural facts about this model. We show that the combinatorics at _ℵω+1${\mathrm{\aleph }}_{\omega +1}$ in this model depend strongly on the properties of _ω1${\omega }_1$ in the ground model. From different ground models for the Cummings–Foreman iteration we can obtain either _ℵω+1∈I[_ℵω+1]${\mathrm{\aleph }}_{\omega +1}\in I[{\mathrm{\aleph }}_{\omega +1}]$ and every stationary subset of _ℵω+1${\mathrm{\aleph }}_{\omega +1}$ reflects or there are a bad scale at _ℵω${\mathrm{\aleph }}_{\omega }$ and a non-reflecting stationary subset of _ℵω+1∩cof(_ω1)${\mathrm{\aleph }}_{\omega +1}\cap \mathrm{cof}({\omega }_1)$. We also prove that regardless of the ground model a strong generalization of the tree property holds at each _ℵn${\mathrm{\aleph }}_n$ for n≥2$n\ge 2$.     

Consistency,optimality, and incompleteness

Assume that the problem _P0$P_0$ is not solvable in polynomial time. Let T   be a first-order theory containing a sufficiently rich part of true arithmetic. We characterize T∪{_ConT}$T\cup \{{\mathit{Con}}_T\}$ as the minimal extension of T   proving for some algorithm that it decides _P0$P_0$ as fast as any algorithm B$\mathbb{B}$ with the property that T   proves that B$\mathbb{B}$ decides _P0$P_0$. Here, _ConT${\mathit{Con}}_T$ claims the consistency of T. As a byproduct, we obtain a version of Gödel?s Second Incompleteness Theorem. Moreover, we characterize problems with an optimal algorithm in terms of arithmetical theories.     

Cardinal characteristics and projective wellorders

Using countable support iterations of S-proper posets, we show that the existence of a definable wellorder of the reals is consistent with each of the following: d<c, b<a=s and b<g.     

Generic embeddings associated to an indestructibly weakly compact cardinal

I use generic embeddings induced by generic normal measures on P_κ(λ) that can be forced to exist if κ is an indestructibly weakly compact cardinal. These embeddings can be applied in order to obtain the forcing axioms in forcing extensions. This has consequences in : The Singular Cardinal Hypothesis holds above κ, and κ has a useful Jónsson-like property. This in turn implies that the countable tower Q_<κ works much like it does when κ is a Woodin limit of Woodin cardinals. One consequence is that every set of reals in the Chang model is Lebesgue measurable and has the Baire Property, the Perfect Set Property and the Ramsey Property. So indestructible weak compactness has effects on cardinal arithmetic high up and also on the structure of sets of real numbers, down low, similar to supercompactness.     

Positive provability logic for uniform reflection principles

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω   corresponds to the full uniform reflection schema, whereas n<ω$n<\omega$ corresponds to its restriction to arithmetical _Πn+1${\Pi }_{n+1}$-formulas. This calculus is shown to be complete w.r.t. a suitable class of finite Kripke models and to be decidable in polynomial time.     

Baumgartnerʼs conjecture and bounded forcing axioms

We study the spectrum of forcing notions between the iterations of σ-closed followed by ccc forcings and the proper forcings. This includes the hierarchy of α-proper forcings for indecomposable countable ordinals α, the Axiom A forcings and forcings completely embeddable into an iteration of a σ-closed followed by a ccc forcing. For the latter class, we present an equivalent characterization in terms of Baumgartner?s Axiom A. This resolves a conjecture of Baumgartner from the 1980s.     

A feasible theory of truth over combinatory algebra

We define an applicative theory of truth _TPT${\mathsf{T}}_{\mathsf{PT}}$ which proves totality exactly for the polynomial time computable functions. _TPT${\mathsf{T}}_{\mathsf{PT}}$ has natural and simple axioms since nearly all its truth axioms are standard for truth theories over an applicative framework. The only exception is the axiom dealing with the word predicate. The truth predicate can only reflect elementhood in the words for terms that have smaller length than a given word. This makes it possible to achieve the very low proof-theoretic strength. Truth induction can be allowed without any constraints. For these reasons the system _TPT${\mathsf{T}}_{\mathsf{PT}}$ has the high expressive power one expects from truth theories. It allows embeddings of feasible systems of explicit mathematics and bounded arithmetic.