Girard’s maxim, that Peano Arithmetic is a theory of one inductive definition, is re-examined in the light of a weak theory EA formalising basic principles of Nelson’s predicative Arithmetic.

This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal's tree theorem, and in particular the connection with the ordinal Γ0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Verlen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to (...) Kruskal, the ‘tree theorem’, as well as a ‘finite miniaturization’ of Kruskal's theorem due to Harvey Friedman. These versions of Kruskal's theorem are remarkable from a proof-theoretic point of view because they are not provable in relatively strong logical systems. They are examples of so-called ‘natural independence phenomena’, which are considered by most logicians as more natural than the metamathematical incompleteness results first discovered by Gödel. Kruskal's tree theorem also plays a fundamental role in computer science, because it is one of the main tools for showing that certain orderings on trees are well founded. These orderings play a crucial role in proving the termination of systems of rewrite rules and the correctness of Knuth-Bendix completion procedures. There is also a close connection between a certain infinite countable ordinal called Γo and Kruskal's theorem. Previous definitions of the function involved in this connection are known to be incorrect, in that, the function is not monotonic. We offer a repaired definition of this function, and explore briefly the consequences of its existence. (shrink)

In this paper we give a new and comparatively simple proof of the following theorem by Girard [1]:“If ∀x∈ ${\cal O}$ ∃y∈ ${\cal O}$ ψ(x,y) (where the relationψ is arithmetic and positive in Kleene's ${\cal O}$ ), then there exists a recursive DilatorD such that ∀α≧ω∀x∈ ${\cal O}$ <α∃y∈ ${\cal O}$ (...) modification of Girard's system in [1]) we construct in a uniform way for each ordinalα a derivation Tα of the formula ∀x ∈ ${\cal O}$ <α∃y∈ ${\cal O}$ ψ(x, y), and then defineD immediately from the family (Tα)α∈On. Especially we set D(α):=Kleene-Brouwer length of (Tα). (shrink)

The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive functions to primitive recursive functions.

This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal's tree theorem, and in particular the connection with the ordinal Γ0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Verlen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to (...) Kruskal, the ‘tree theorem’, as well as a ‘finite miniaturization’ of Kruskal's theorem due to Harvey Friedman. These versions of Kruskal's theorem are remarkable from a proof-theoretic point of view because they are not provable in relatively strong logical systems. They are examples of so-called ‘natural independence phenomena’, which are considered by most logicians as more natural than the metamathematical incompleteness results first discovered by Gödel. Kruskal's tree theorem also plays a fundamental role in computer science, because it is one of the main tools for showing that certain orderings on trees are well founded. These orderings play a crucial role in proving the termination of systems of rewrite rules and the correctness of Knuth-Bendix completion procedures. There is also a close connection between a certain infinite countable ordinal called Γo and Kruskal's theorem. Previous definitions of the function involved in this connection are known to be incorrect, in that, the function is not monotonic. We offer a repaired definition of this function, and explore briefly the consequences of its existence. (shrink)

Journal of Mathematical Logic, Volume 23, Issue 02, August 2023. In mathematical logic there are two seemingly distinct kinds of principles called “reflection principles.” Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic reflection principles assert that every provable sentence from some complexity class is true. In this paper, we study connections between these two kinds of reflection principles in the setting of second-order arithmetic. We prove that, for (...) a large swathe of theories, [math]-model reflection is equivalent to the claim that arbitrary iterations of uniform [math] reflection along countable well-orderings are [math]-sound. This result yields uniform ordinal analyzes of theories with strength between [math] and [math]. The main technical novelty of our analysis is the introduction of the notion of the proof-theoretic dilator of a theory [math], which is the operator on countable ordinals that maps the order-type of [math] to the proof-theoretic ordinal of [math]. We obtain precise results about the growth of proof-theoretic dilators as a function of provable [math]-model reflection. This approach enables us to simultaneously obtain not only [math], [math] and [math] ordinals but also reverse-mathematical theorems for well-ordering principles. (shrink)

A hierarchy (J D g ) D Dilator of ordinal functionsJ D g : On→On is introduced and studied. It is a hierarchy of iterations relative to some giveng:OnarOn, defined by primitive recursion on dilators. This hierarchy is related to a Bachmann hierarchy $\left( {\phi _\alpha ^g } \right)_{\alpha< \varepsilon _{\Omega {\mathbf{ }} + {\mathbf{ }}1} }$ , which is built on an iteration ofg ↑ Ω as initial function.This Bachmann hierarchy $\left( {\phi _\alpha ^g } \right)_{\alpha< \varepsilon _{\Omega {\mathbf{ (...) }} + {\mathbf{ }}1} }$ itself is shown to be explicitly definable by $$\phi _\alpha ^g (\eta ) = g^{\Omega ^\alpha \cdot (1 + \eta )} (0)$$ from a hierarchy of iterationsg α :Ω→Ω for weakly monotonicg: Ω→Ω withg(0)>0. Forg=λη. (1+η) ·ω org=λη. 1, in particular, one obtains as $\left( {\phi _\alpha ^g } \right)_{\alpha< \varepsilon _{\Omega {\mathbf{ }} + {\mathbf{ }}1} }$ Bachmann hierarchy.With every ordinalα≦ε Ω+1 a dilatorD α is associated.D α is “below” the dilator $$\left( {\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{2} + Id} \right)_{(\omega )}$$ , which is defined as $$\mathop {\sup }\limits_{n< \omega } (\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{2} + Id)_{(n)}$$ with (¯2+Id)(0):=1 and $$(\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{2} + Id)_{(n + 1)} : = (\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{2} + Id)^{(2 + Id)_{(n)} }$$ . For weakly monotonicg:OnarOn satisfyingg(0)>0 and $g(\Omega ) \subseteqq \Omega$ , and forη<Ω andα<ε Ω+1 it is proved that. (shrink)

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality. We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals (...) grow very rapidly. Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it. We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank. The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area. Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy. Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result. (shrink)

The notion of a “ptyx” is formalised in second-order arithmetic, and, using proof-theoretic techniques based on sequent-calculus, bounds are obtained for the ptykes of type 1 and 2 which can be proved to be ptykes using arithmetic comprehension.

Applying Woodin's non-stationary tower notion of forcing, I prove that the existence of a supercompact cardinal κ in V and a Ramsey dilator in some small forcing extension V[G] implies the existence in V of a measurable dilator of size κ, measurable by κ-complete measures.

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)

We give a simple proof ofΠ 1 1 andΠ 2 1 uniformization results, which is based on the use ofΠ 2 1 -Logic.

Subrecursive hierarchy classifications are used to compare the complexities of recursive functions according to their derivations in a version of Kleene's equation calculus, and their computations by term-rewriting. In each case ordinal bounds are assigned, and it turns out that the respective complexity measures are given by a version of the Fast Growing Hierarchy, and the Slow Growing Hierarchy. Known comparisons between the two hierarchies then provide ordinal trade-offs between derivation and computation. Characteristics of some well-known subrecursive classes are also (...) read off. (shrink)

The class of all recursive functions fails to possess a natural hierarchical structure, generated predicatively from "within". On the other hand, many (proof-theoretically significant) sub-recursive classes do. This paper attempts to measure the limit of predicative generation in this context, by classifying and characterizing those (predictably terminating) recursive functions which can be successively defined according to an autonomy condition of the form: allow recursions only over well-orderings which have already been "coded" at previous levels. The question is: how can a (...) recursion code a well-ordering? The answer lies in Girard's theory of dilators, but is reworked here in a quite different and simplified framework specific to our purpose. The "accessible" recursive functions thus generated turn out to be those provably recursive in $(\prod_{1}^{1}-CA)_{0}$. (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)

We study increasing F-sequences, where F is a dilator: an increasing F-sequence is a sequence (indexed by ordinal numbers) of ordinal numbers, starting with 0 and terminating at the first step x where F(x) is reached (at every step x + 1 we use the same process as in decreasing F-sequences, cf. [2], but with "+ 1" instead of "- 1"). By induction on dilators, we shall prove that every increasing F-sequence terminates and moreover we can determine for every dilator (...) F the point where the increasing F-sequence terminates. We apply these results to inverse Goodstein sequences, i.e. increasing (1 + Id) (ω) -sequences. We show that the theorem every inverse Goodstein sequence terminates (a combinatorial theorem about ordinal numbers) is not provable in ID 1 . For a general presentation of the results stated in this paper, see [1]. We use notions and results concerning the category ON (ordinal numbers), dilators and bilators, summarized in [2, pp. 25-31]. (shrink)

We present a list of open questions in reverse mathematics, including some relevant background information for each question. We also mention some of the areas of reverse mathematics that are starting to be developed and where interesting open question may be found.

We prove a strong boundedness theorem for dilators: if A ⊆ DIL is Σ 1 1 , then there is a recursive dilator D 0 such that ∀ D ∈ A.

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 main theorem of this paper is: If ƒ is a partial function from 1 to 1 which is ∑11-bounded, then there is a weakly finite primitive recursive dilatorD such that for all infinite αεdom, ƒ D. The proof involves only elementary combinatorial constructions of trees. A generalization to ptykes is also given.

It is shown that the so called slow growing hierarchy depends non trivially on the choice of its underlying structure of ordinals. To this end we investigate the growth rate behaviour of the slow growing hierarchy along natural subsets of notations for $\Gamma_0$. Let T be the set-theoretic ordinal notation system for $\Gamma_0$ and $T^{tree}$ the tree ordinal representation for $\Gamma$. It is shown in this paper that $_{\alpha \in T}$ matches up with the class of functions which are elementary (...) recursive in the Ackermann function as does $_{\alpha \in T^{tree}}$. By thinning out terms in which the addition function symbol occurs we single out subsystems $T* \subseteq T$ and $T^{tree*} \subseteq T^{tree}$ and prove that $_{\alpha \in T^{tree*}}$ still matches up with $_{\alpha \in T^{tree}}$ but $_{\alpha \in T*}$ now consists of elementary recursive functions only. We discuss the relationship between these results and the $\Gamma_0$-based termination proof for the standard rewrite system for the Ackermann function. (shrink)

Let Ω be the least uncountable ordinal. Let K(Ω) be the category where the objects are the countable ordinals and where the morphisms are the strictly monotonic increasing functions. A dilator is a functor on K(Ω) which preserves direct limits and pullbacks. Let $\tau \Omega: \xi = \omega^\xi\}$ . Then τ has a unique "term"-representation in Ω. λξη.ω ξ + η and countable ordinals called the constituents of τ. Let $\delta and K(τ) be the set of the constituents of τ. (...) Let β = max K(τ). Let [ β ] be an occurrence of β in τ such that τ [ β] = τ. Let $\bar \theta$ be the fixed point-free version of the binary Aczel-Buchholz-Feferman-function (which is defined explicitly in the text below) which generates the Bachman-hierarchy of ordinals. It is shown by elementary calculations that $\xi \mapsto \bar \theta(\tau \lbrack \gamma + \xi \rbrack)\delta$ is a dilator for every $\gamma > \max\{\beta. \delta.\omega\}$. (shrink)

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

The main theorem of this paper is: If ƒ is a partial function from ℵ 1 to ℵ 1 which is ∑ 1 1 -bounded, then there is a weakly finite primitive recursive dilator D such that for all infinite αϵdom , ƒ ⩽ D . The proof involves only elementary combinatorial constructions of trees. A generalization to ptykes is also given.

It is generally accepted that H. Friedman’s gap condition is closely related to iterated collapsing functions from ordinal analysis. But what precisely is the connection? We offer the following answer: In a previous paper we have shown that the gap condition arises from an iterative construction on transformations of partial orders. Here we show that the parallel construction for linear orders yields familiar collapsing functions. The iteration step in the linear case is an instance of a general construction that we (...) call ‘Bachmann–Howard derivative’. In the present paper, we focus on the unary case, i.e., on the gap condition for sequences rather than trees and, correspondingly, on addition-free ordinal notation systems. This is partly for convenience, but it also allows us to clarify a phenomenon that is specific to the unary setting: As shown by van der Meeren, Rathjen and Weiermann, the gap condition on sequences admits two linearizations with rather different properties. We will see that these correspond to different recursive constructions of sequences. (shrink)