The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the proof-theoretic strengths (...) of the consistent theories? The first question was answered completely by Friedman and Sheard; all subsets of the Optional Axioms were classified as either consistent or inconsistent giving rise to nine maximal consistent theories of truth.They also determined the proof-theoretic strength of two subsets of the Optional Axioms. The aim of this paper is to continue the work begun by Friedman and Sheard. We will establish the proof-theoretic strength of all the remaining seven theories and relate their arithmetic part to well-known theories ranging from PA to the theory of ${\Sigma^1_1}$ dependent choice. (shrink)

We present a new manifestation of Gödel’s second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert’s program. Specifically, we consider a proper extension of Peano arithmetic ( $\mathbf {PA}$ ) by a mathematically meaningful axiom scheme that consists of $\Sigma ^0_2$ -sentences. These sentences assert that each computably enumerable ( $\Sigma ^0_1$ -definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is (...) relevant for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel’s second incompleteness theorem. In contrast, Gödel’s theorem is not needed for typical examples of $\Pi ^0_2$ -independence (such as the Paris–Harrington principle), since computational strength provides an extensional invariant on the level of $\Pi ^0_2$ -sentences. (shrink)

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$, $$\begin{align*}T_0+ \mathrm{RFN}_{\varPi^1_{n+2}} \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}, \end{align*}$$ $$\begin{align*}T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}} \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}^{-}, \end{align*}$$ where T is $T_0$ augmented with full induction, and $\mathrm {TI}_{\varPi ^1_n}^{-}$ denotes the schema of transfinite induction up (...) to $\varepsilon _0$ for $\varPi ^1_n$ formulas without set parameters. (shrink)

We introduce strong Goodstein principles which are true but unprovable in strong impredicative theories like IDn.

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...) we prove in this paper that the statement “if X is well-ordered then εX is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a fragment of. (shrink)

Gödel’s first incompleteness result from 1931 states that there are true assertions about the natural numbers which do not follow from the Peano axioms. Since 1931 many researchers have been looking for natural examples of such assertions and breakthroughs were obtained in the seventies by Jeff Paris [Some independence results for Peano arithmetic. J. Symbolic Logic 43 725–731] , Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977] and Laurie Kirby [L. Kirby, Jeff Paris, Accessible independence results for Peano Arithmetic, Bull. of (...) the LMS 14 285–293]) and Harvey Friedman [S.G. Simpson, Non-provability of certain combinatorial properties of finite trees, in: Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam, 1985, pp. 87–117; R. Smith, The consistency strength of some finite forms of the Higman and Kruskal theorems, in: Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam, 1985, pp. 119–136] who produced the first mathematically interesting independence results in Ramsey theory and well-order and well-quasi-order theory .In this article we investigate Friedman-style principles of combinatorial well-foundedness for the ordinals below ε0. These principles state that there is a uniform bound on the length of decreasing sequences of ordinals which satisfy an elementary recursive growth rate condition with respect to their Gödel numbers.For these independence principles we classify their phase transitions, i.e. we classify exactly the bounding conditions which lead from provability to unprovability in the induced combinatorial well-foundedness principles.As Gödel numbering for ordinals we choose the one which is induced naturally from Gödel’s coding of finite sequences from his classical 1931 paper on his incompleteness results.This choice makes the investigation highly non-trivial but rewarding and we succeed in our objectives by using an intricate and surprising interplay between analytic combinatorics and the theory of descent recursive functions. For obtaining the required bounds on count functions for ordinals we use a classical 1961 Tauberian theorem of Parameswaran which apparently is far remote from Gödel’s theorem. (shrink)

The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference . As a result, PA+Con is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which (...) PA+Con is the least “natural” theory whose strength is greater than that of PA? In this paper we exhibit natural theories in strength strictly between PA and PA+Con by introducing a notion of slow consistency. (shrink)

Let T(Ω) be the ordinal notation system from Buchholz-Schütte (1988). [The order type of the countable segmentT(Ω)0 is — by Rathjen (1988) — the proof-theoretic ordinal the proof-theoretic ordinal ofACA 0 + (Π 1 l −TR).] In particular let ↦Ω a denote the enumeration function of the infinite cardinals and leta ↦ ψ0 a denote the partial collapsing operation on T(Ω) which maps ordinals of T(Ω) into the countable segment TΩ 0 of T(Ω). Assume that the (fast growing) extended Grzegorczyk (...) hierarchy $(F_a )_{a \in T(\Omega )_0 }$ and the slow growing hierarchy $(G_a )_{a \in T(\Omega )_0 }$ are defined with respect to the natural system of distinguished fundamental sequences of Buchholz and Schütte (1988) in the following way: $$\begin{array}{*{20}c} {G_0 (n): = 0,} & {F_0 (n): = (n + 1)^2 ,} \\ {\begin{array}{*{20}c} {G_{a + 1} (n): = G_a (n) + 1,} \\ {G_l (n): = G_{l[n]} (n),} \\ \end{array} } & {\begin{array}{*{20}c} {F_{a + 1} (n): = \underbrace {F_a (...F_a }_{n + 1 - times}(n)...),} \\ {F_l (n): = F_{l[n]} (n),} \\ \end{array} } \\ \end{array}$$ wherel is a countable limit ordinal (term) and (l[n]) n ∈N is the distinguished fundamental sequence assigned tol. For each ordinal (term)a in T(Ω) and each natural numbern letC n (a) be the formal term which results from the ordinal terma by successively replacing every occurence ofψ a by $\psi _{ - 1 + C_n (a)}$ whereψ −1 is considered as a defined function symbol, namely $\psi _{ - 1} b: = F_{\psi _0 b + 1} (n + 1)$ . (Note thatψ a 0=Ω a ) In this article it is shown that for each ordinal termψ 0 a in T(Ω) there exists a natural numbern 0 such thatψ 0 C n (a) ∈ T(Ω) and $G_{\psi _0 a} (n) \leqslant F_{\psi _0 C_n (a) + 1} (n + 1)$ holds for alln≥n 0. This hierarchy comparison theorem yields a plethora of new results on nontrivial lower bounds for the slow growing ordinals — i.e. ordinals for which the slow growing hierarchy yields a classification of the provably total functions of the theory in question — of various theories of iterated inductive definitions (and subsystems ofKPi) and on the number and size of the subrecursively inaccessible ordinals — i.e. ordinals at which the extended Grzegorczyk hierarchy and the slow growing hierarchy catch up — below the proof-theoretic ordinal ofACA 0+(Π 1 l −TR). In particular these subrecursively inaccessibles ordinals are necessarily of the form $\psi _0 \Omega ..._{\Omega _\omega }$. (shrink)

The 1-consistency of arithmetic is shown to be equivalent to the existence of fixed points of a certain type of update procedure, which is implicit in the epsilon-substitution method.

We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as well as seems possible the intrinsic computational character of the standard cut elimination process. The article is intended to be suitable for teaching purposes and just requires basic familiarity with PA and the ordinals below ε0. (Familiarity with a cut elimination theorem for a Gentzen or Tait calculus is helpful but not presupposed).

We survey a selection of results about majorization hierarchies. The main focus is on classical and recent results about the comparison between the slow and fast growing hierarchies.

Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte (...) treatment of Gödel's T and utilizes the collapsing function ψ: ε 0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [] 0 is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Gödel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T n be the subsystem of T in which the recursors have type level less than or equal to n+2. (By definition, case distinction functionals for every type are also contained in T n .) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the T n -derivation lengths in terms of ω n+2 -descent recursive functions. The derivation lengths of type one functionals from T n (hence also their computational complexities) are classified optimally in terms of $ -descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T 0 is primitive recursive, thus any type one functional a in T 0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T 1 in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the IΣ n+1 -provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO ( $\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ( $\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I Σ n+1 ), hence PRA + PRWO( $\epsilon_0) \vdash$ Con(PA) and PRA + PRWO( $\omega_{n+2}) \vdash$ Con(IΣ n+1 ). For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity. (shrink)

Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of $PA, PA + TI(\prec\lceil)$ (where it is assumed that the well-ordering $\prec$ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.

For α less than ε0 let $N\alpha$ be the number of occurrences of ω in the Cantor normal form of α. Further let $\mid n \mid$ denote the binary length of a natural number n, let $\mid n\mid_h$ denote the h-times iterated binary length of n and let inv(n) be the least h such that $\mid n\mid_h \leq 2$ . We show that for any natural number h first order Peano arithmetic, PA, does not prove the following sentence: For all (...) K there exists an M which bounds the lengths n of all strictly descending sequences $\langle \alpha_0, ..., \alpha_n\rangle$ of ordinals less than ε0 which satisfy the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid \cdot \mid i\mid_h$ . As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence $\langle \alpha_0,..., \alpha_n\rangle$ of ordinals less than ε0 which satisfies the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid\cdot inv(i)$ . The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations. Using results from Otter and from Matou $\breve$ ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856... (shrink)

An approach to ordinal analysis is presented which is finitary, but highlights the semantic content of the theories under consideration, rather than the syntactic structure of their proofs. In this paper the methods are applied to the analysis of theories extending Peano arithmetic with transfinite induction and transfinite arithmetic hierarchies.

Weiermann [18] introduces a new method to generate fast growing functions in order to get an elegant and perspicuous proof of a bounding theorem for provably total recursive functions in a formal theory, e.g., in PA. His fast growing function θαn is described as follows. For each ordinal α and natural number n let T α n denote a finitely branching, primitive recursive tree of ordinals, i.e., an ordinal as a label is attached to each node in the tree so (...) that the labelling is compatible with the tree ordering. Then the tree T α n is well founded and hence finite by Konig's lemma. Define θαn=the depth of the tree T α n =the length of the longest branch in T α n . We introduce new fast and slow growing functions in this mode of definitions and show that each of these majorizes provably total recursive functions in PA. (shrink)