E. Combinatorial Independence Results

Results that have been achieved through ordinal analysis mainly fall into four groups: (1) Consistency of subsystems of classical second order arithmetic and set theory relative to constructive theories, (2) reductions of theories formulated as conservation theorems, (3) combinatorial independence results, and (4) classifications of provable functions and ordinals. In this appendix we shall just provide a few examples of (3).^[56] (4) is to be discussed in Appendix F.

Gödel’s Incompleteness Theorems raised the question of whether there is a strictly mathematical example of an incompleteness in first-order Peano arithmetic and stronger systems, one which is mathematically simple and interesting and does not require the numerical coding of metamathematical notions. The first such examples were found by Gentzen and Goodman. Recall from section 3 the ordinal representation for ${\epsilon }_0$ based on Cantor’s normal form with its ordering $\prec$. Let PRWO$({\epsilon }_0)$ be the statement that there are no infinite primitive recursive $\prec$-descending sequences.

This theorem is not explicitly stated in his 1938b but it is an immediate consequence of his consistency proof of PA.^[57] Goodstein, upon studying Gentzen’s 1936, established a connection between descending sequences of ordinals below ${\epsilon }_0$ and certain sequences of natural numbers. He realized that given two ordinals $\alpha ,\beta <{\epsilon }_0$ one could replace the base $\omega$ in their complete Cantor normal forms by a sufficiently large number b and the resulting natural numbers ${\hat{\mathrm{T}}}_b^{\omega }(\alpha )$ and ${\hat{\mathrm{T}}}_b^{\omega }(\beta )$ would stand in the same ordering as $\alpha$ and $\beta$. This is a consequence of the fact that the criteria for comparing ordinals in Cantor normal form are the same as for natural numbers in complete base b-representation. There is a Cantor normal form for positive integers m to any base b with $b\ge 2$, namely we can express m uniquely in the form

$$\begin{array}{}\text{(e1)}& m=b^{n_1}\cdot k_1+\dots +b^{n_r}\cdot k_r\end{array}$$

where $m>n_1>\dots >n_r\ge 0$ and $0<k_1,\dots ,k_r<b$. As each $n_i>0$ is itself of this form we can repeat this procedure, arriving at what is called the complete b-representation of m. In this way we get a unique representation of m over the alphabet $0,1,\dots ,b,+,\cdot$.

For example

$$\begin{array}{rl}7625597485157& =3^{27}\cdot 1+3^4\cdot 2+3^1\cdot 2+3^0\cdot 2\\ & =3^{3^3}+3^{3+1}\cdot 2+3^1\cdot 2+2.\end{array}$$

In 1944 Goodstein defined what came to be called Goodstein sequences.

Goodstein proved that all Goodstein sequences are finite. From his work combined with that of Gentzen 1938b he could have concluded the following result (see Rathjen 2015: Theorem 2.9).

Already the termination of special Goodstein sequences, i.e., those where the base change is governed by the shift function, is not provable in PA. This result was obtained only much later by Kirby and Paris (1982) using model-theoretic tools. The latter prompted Cichon (1983) to find a different (short) proof that harked back to older proof-theoretic work of Kreisel (1952) which identified the so-called $<{\epsilon }_0$-recursive functions as the provably recursive functions of PA; see Appendix F, Definition F.1. Other results pivotal to Cichon (1983) were ordinal-recursion-theoretic classifications of Schwichtenberg (1971) and Wainer (1970) which showed that the latter class of recursive functions consists exactly of those elementary in one of the fast growing functions $F_{\alpha }$ with $\alpha <{\epsilon }_0$. As $F_{{\epsilon }_0}$ eventually dominates any of these functions it is not provably total in PA. Cichon verified that $F_{{\epsilon }_0}$ is elementary in the function $f_{\text{good}}$ of Definition E.2. Thus termination of special Goodstein sequences is not provable in PA.^[58]

Mathematical independence results enjoyed great popularity in the 1970s and 1980s. Perhaps the most elegant of these is a strengthening of the Finite Ramsey Theorem due to Paris and Harrington (1977). The original proofs of the independence of combinatorial statements from PA all used techniques from non-standard models of arithmetic. Only later on alternative proofs using proof-theoretic techniques were found. However, results from ordinal-theoretic proof theory turned out to be pivotal in providing independence results for theories stronger than PA, and even led to a new combinatorial statement. The stronger theories referred to are Friedman’s system ${\mathbf{\text{ATR}}}_0$ of arithmetical transfinite recursion and the system $({\mathrm{\Pi }}_1^1\text{-}\mathbf{\text{CA}}{)}_0$ based on ${\mathrm{\Pi }}_1^1$-comprehension. The independent combinatorial statements have their origin in certain embeddability questions in the theory of finite graphs. The first is a famous theorem of Kruskal asserting that every set of finite trees has only finitely many minimal elements.

The proof of the above independence result exploits a connection between finite trees and ordinal representations for ordinals $<{\mathrm{\Gamma }}_0$ and the fact that ${\mathrm{\Gamma }}_0$ is the proof-theoretic ordinal of ${\mathbf{\text{ATR}}}_0$. Each ordinal representation $\mathfrak{a}$ is assigned a finite tree ${\mathbb{B}}_{\mathfrak{a}}$ to the effect that for two representations $\mathfrak{a}$ and $\mathfrak{b}$, ${\mathbb{B}}_{\mathfrak{a}}\le {\mathbb{B}}_{\mathfrak{b}}$ implies $\mathfrak{a}\le \mathfrak{b}$. Hence Kruskal’s theorem implies the well-foundedness of ${\mathrm{\Gamma }}_0$ and is therefore not provable in ${\mathbf{\text{ATR}}}_0$. The connection between finite trees and ordinal representations for ordinals $<{\mathrm{\Gamma }}_0$ was noticed by Friedman (cf. Simpson 1985) and independently by Diana Schmidt (1979).

A hope in connection with ordinal analyses is that they may lead to discoveries of new combinatorial principles which encapsulate considerable proof-theoretic strength. Examples are still scarce. One case where ordinal notations led to a new combinatorial result was Friedman’s extension of Kruskal’s Theorem, EKT, which asserts that finite trees are well-quasi-ordered under gap embeddability (see Simpson 1985). The gap condition imposed on the embeddings is directly related to an ordinal notation system that was used for the analysis of ${\mathrm{\Pi }}_1^1$ comprehension. The principle EKT played a role in the proof of the graph minor theorem of Robertson and Seymour.

The proof of Theorem E.10 employs the ordinal representation system of section 5.3.1. for the proof-theoretic ordinal of $({\mathrm{\Pi }}_1^1-\mathbf{\text{CA}}{)}_0$ which is ${\psi }_{{\mathrm{\Omega }}_1}({\mathrm{\Omega }}_{\omega })$. The connection between $<\omega$ labeled trees and this ordinal is that $\mathrm{\forall }n<\omega \text{WQO}({\mathcal{B}}_n)$ implies the well-foundedness of ${\psi }_{{\mathrm{\Omega }}_1}({\mathrm{\Omega }}_{\omega })$ (on the basis of ${\mathbf{\text{ACA}}}_0$ say). The connection is even closer in that the gap condition imposed on the embeddings between trees is actually gleaned from the ordering of the ordinal representations. If one views these terms as labeled trees, then the gap condition is exactly what one needs to ensure that an embedding of two such trees implies that the ordinal corresponding to the first tree is less than the ordinal corresponding to the second tree. It is also for that reason that criticism had been leveled against the principle EKT for being too contrived or too metamathematical. But this was superseded by the role that EKT played in the proof of the graph minor theorem (see Friedman, Robertson, & Seymour 1987).

As to the importance attributed to the graph minor theorem, let us quote from a book on Graph Theory:

Our goal […] is a single theorem, one which dwarfs any other result in graph theory and may doubtless be counted among the deepest theorems that mathematics has to offer: in every infinite set of graphs there are two such that one is a minor of the other. This minor theorem, inconspicuous though it may look at first glance, has made a fundamental impact both outside graph theory and within. Its proof, due to Neil Robertson and Paul Seymour, takes well over 500 pages. (Diestel 1997: 249)

As a corollary to the graph minor theorem one obtains positive answers to two famous conjectures.

A further independence result that ensues from ordinal analysis is due to Buchholz (1987). It concerns an extension of the hydra game of Kirby and Paris. It is shown in that paper that the assertion that Hercules has a winning strategy in this game is not provable in the theory $({\mathrm{\Pi }}_1^1-\mathbf{\text{CA}})+\mathbf{\text{BI}}$.

It would be very desirable to also find mathematically fruitful combinatorial principles hidden in stronger representation systems such as the ones based on Mahlo cardinals and weakly compact cardinals used for analyzing Kripke-Platek set theory with a recursively Mahlo universe and with ${\mathrm{\Pi }}_3$-reflection, respectively.