2 Stage I: Gödel’s Doctrine and consistency statements

2.1 Stage I(a): Which comprehension schema do we need to prove Con(PA)?

As mentioned above, implicit in Gödel’s view from [Reference Gödel, Feferman, Dawson, Kleene, Moore, Solovay and Heijenoort51] is the result that the impredicative second-order axioms for arithmetic (or set theory) prove the consistency of the first-order versions of these axioms. Gödel’s implicit result holds because (i) the theories in question are essentially reflexive and (ii) the relevant first-order theories are sub-theories of a finite fragment of their respective second-order theories.Footnote ¹⁵

In the first stage of his argument against GD, Feferman (also implicitly) appeals to this result and then shows that its full strength is not required. Let us begin with some key notation and definitions.

We write $\mathsf {L}_{1}$ for the language of first-order Peano arithmetic. This has only one sort of variable (number variables $n, m, \ldots $ ) intended to range over the natural numbers $\omega = \left \{0, 1, 2, \ldots \right \}$ . We write PA for the formal system of first-order Peano arithmetic. PA consists of: (i) universal closures of $\mathsf {L}_{1}$ -formulas expressing the basic number-theoretic axioms and (ii) an induction schema

(1) $$ \begin{align} (\varphi(0) \wedge \forall n (\varphi(n) \rightarrow \varphi(n+1))) \rightarrow \forall n\, \varphi(n) \end{align} $$

for each $\varphi \in \mathsf {L}_{1}$ . We now extend $\mathsf {L}_{1}$ to $\mathsf {L}_{2}$ , the language of second-order arithmetic, by adding set variables and quantifiers to $\mathsf {L}_{1}$ along with a new binary relation symbol $\in $ between numbers and sets. Second-order Peano arithmetic, ${\mathsf {PA}}_{2}$ , consists of: (i) the universal closures of $\mathsf {L}_{2}$ -formulas expressing the basic number-theoretic axioms; (ii) an induction schema

(2) $$ \begin{align} (0 \in X \wedge \forall n(n \in X \rightarrow n+1 \in X)) \rightarrow \forall n(n \in X); \end{align} $$

and (iii) a comprehension schema

(3) $$ \begin{align} \exists X \forall n(n \in X \leftrightarrow \varphi(n)), \end{align} $$

where $\varphi (n)$ is any formula in $\mathsf {L}_{2}$ in which X does not occur freely.Footnote ¹⁶ $(\varphi (n)$ may contain further free variables besides n.) Feferman’s argument deals with the particular comprehension schema required to prove the canonical consistency statement for PA, Con(PA).

For a class of formulas $\Phi $ , we write the comprehension schema for formulas in $\Phi $ as $\Phi $ -CA. Following the practice of reverse mathematics, $\Phi $ -CA will from now on be an abbreviation for the subsystemFootnote ¹⁷ of ${\mathsf {PA}}_{2}$ obtained by replacing the full comprehension schema in (3) with ${\Phi }$ -CA and using full second-order induction, i.e., the universal closure of

(4) $$ \begin{align} (\varphi(0) \wedge \forall n(\varphi(n) \rightarrow \varphi(n+1))) \rightarrow \forall n \, \varphi(n), \end{align} $$

where $\varphi (n)$ is any $\mathsf {L}_{2}$ formula. $\Phi $ - $\mathsf {CA}_{0}$ is defined similarly, except now the subsystem uses the more restricted form of induction in (2), indicated by the “0” subscript.

Finally, an $\mathsf {L}_{2}$ -formula is said to be arithmetical if it contains no set quantifiers. Among arithmetical formulas, a formula $\varphi $ is said to be $\Pi ^{0}_{1}$ if it has the form $\forall n\, \theta $ , where $\theta $ has only bounded quantifiers. Similarly, $\varphi $ is said to be $\Sigma ^{0}_{1}$ if it has the form $\exists n \, \theta $ where $\theta $ has only bounded quantifiers. Finally, $\varphi $ is said to be $\Delta ^{0}_{1}$ if it is both $\Pi ^{0}_{1}$ and $\Sigma ^{0}_{1}$ . Con(PA) is a $\Pi ^{0}_{1}$ statement since

(5) $$ \begin{align} {\mathsf{Con}}({\mathsf{PA}}):= \forall n \neg \mathsf{Proof}_{{\mathsf{PA}}}(n, \ulcorner 0=1 \urcorner), \end{align} $$

where $\mathsf {Proof}_{{\mathsf {PA}}}(n, \ulcorner \varphi \urcorner )$ is a primitive recursive relation expressing that n is the Gödel number/code of a proof in PA of the statement $\varphi $ with Gödel number $\ulcorner \varphi \urcorner $ , i.e., $\ulcorner \varphi \urcorner $ is the code of the proof’s endformula. Finally, we define the provability predicate for PA as $\mathsf {Prov}_{{\mathsf {PA}}}(x):= \exists y\, \mathsf {Proof}_{{\mathsf {PA}}}(y, x)$ .

In outline, Feferman’s argument is as follows. First, he shows that an extension of PA to ${\mathsf {PA}}_{2}$ with appropriate comprehension schema suffices to define (i) $\mathsf {Tr}_{1}(x)$ , the formal truth definition for $\mathsf {L}_{1}$ and (ii) the set of Gödel numbers of true statements in PA. Second, he shows that our extension proves $\mathsf {Prov}_{{\mathsf {PA}}}(\ulcorner \varphi \urcorner ) \rightarrow \mathsf {Tr}_{1}(\ulcorner \varphi \urcorner )$ , viz., the formal statement expressing that provability in PA entails truth. Con(PA) follows as a special case of this schema when we let $\varphi $ be a refutable sentence like $\bot := (0=1)$ , and so the adjunction of higher-order principles allows us to prove new finitary statements.Footnote ¹⁸

Begin by letting $\Gamma $ be the set of Gödel numbers of true statements in PA. Gödel’s implicit result suggests that we use $\Pi ^{1}_{1}$ -CA to define $\Gamma $ . An $\mathsf {L}_{2}$ -formula is said to be $\Pi ^{1}_{1}$ if it has the form $\forall X\, \theta $ , where X is a set variable and $\theta $ is arithmetical. Thus, the comprehension schema of this system

(6) $$ \begin{align} \exists X\, \forall n(n \in X \leftrightarrow \varphi(n)), \end{align} $$

for all $\Pi ^{1}_{1}$ formulas $\varphi $ , is expressly impredicative since we quantify over the full powerset $\mathscr {P}(\mathbb {N})$ in order to define X. Thus, in order to avoid this impredicative definition and thereby undermine GD, Feferman must show that a weaker system (with weaker comprehension schema) suffices to define $\Gamma $ and to prove Con(PA). Indeed, he shows that we can make do with $\Delta ^{1}_{1}$ -CA.Footnote ¹⁹ $\!\!\!^{,}$ Footnote ²⁰ Thus, since Con(PA) is a true $\Pi ^{0}_{1}$ statement not provable in PA, the adjunction of “higher types,” viz., our extension of PA to the subsystem $\Delta ^{1}_{1}$ -CA, suffices to prove previously undecidable statements with finitary content.

2.2 Discussion of Stage I(a)

A few comments are now in order. First, although Feferman does not remark upon this (presumably because he goes on to give an argument for deciding Con(PA) without set-theoretical principles), the above considerations already undermine GD. This is because, while it is true that we have added “higher set-theoretical types” to PA in order to prove Con(PA), we have done so using innocuous higher types. By Feferman’s lights, we run into trouble only when we use the full power-set, $\mathscr {P}(\mathbb {N})$ , as this is what embroils us in a platonistic conception of mathematics. However, $\Delta ^{1}_{1}$ -CA requires only a fragment of the full powerset, and thus does not necessarily commit one to platonism.

One might still be concerned, however, since $\Delta ^{1}_{1}$ -CA is prima facie impredicative (though less radically so than $\Pi ^{1}_{1}$ -CA). In response to this worry, one can appeal to the following result that shows $\Delta ^{1}_{1}$ -CA is “proof-theoretically reducible” to a predicatively justified system.Footnote ²¹

We write ${\mathsf {ACA_{0}}}$ for the subsystem of ${\mathsf {PA}}_{2}$ consisting of the axioms of PA, the induction schema in (2), and the universal closure of

(7) $$ \begin{align} \exists X\, \forall n (n \in X \leftrightarrow \varphi(n)) \end{align} $$

with $\varphi (n)$ arithmetical and in which X does not occur freely. We then write $\mathsf {ACA}$ for the subsystem of ${\mathsf {PA}}_{2}$ consisting of the same axioms as ${\mathsf {ACA_{0}}}$ but now with full second-order induction. Next, given a natural well-ordering $<_{\alpha }$ of order-type $\alpha $ , $(\mathsf {ACA})_{\alpha }$ denotes the iteration of $\mathsf {ACA}$ along $<_{\alpha }$ and $(\mathsf {ACA})_{<\alpha }$ denotes the union of the $(\mathsf {ACA})_{\beta }$ with $\beta < \alpha $ . We now consider such iterated systems up to certain recursive ordinals. According to the widely accepted characterization of predicativity (given the natural numbers) by Feferman and Schütte, the least non-predicatively provable ordinal is $\Gamma _{0}$ , the Feferman–Schütte ordinal.Footnote ²² Since $\epsilon _{0} < \Gamma _{0}$ , where $\epsilon _{0}$ is the proof-theoretic ordinalFootnote ²³ of PA, $\mathsf {ACA}_{<\epsilon _{0}}$ is predicatively justified.Footnote ²⁴ The crucial result then states that

(8) $$ \begin{align} \Delta^{1}_{1}\text{-}\mathsf{CA} \leq \mathsf{ACA}_{<\epsilon_{0}} \end{align} $$

for $\Pi ^{1}_{2}$ -sentences, viz., $\Delta ^{1}_{1}$ -CA is proof-theoretically reducible to $\mathsf {ACA}_{<\epsilon _{0}}$ for $\Pi ^{1}_{2}$ -sentences. This justifies the claim that $\Delta ^{1}_{1}$ -CA, despite appearances, is a predicatively justified system. Hence, by Feferman’s lights, its use in proving Con(PA) is a genuinely innocuous use of the infinite.Footnote ²⁵

Second, as Feferman was surely aware, we can get away with even less than $\Delta ^{1}_{1}$ -CA in proving Con(PA), which would strengthen his argument against GD in this case. In particular, it is well-known that ${\mathsf {ACA_{0}}}$ is a conservative extension of PA, i.e., every sentence in $\mathsf {L}_{1}$ provable in ${\mathsf {ACA_{0}}}$ is also provable in PA.Footnote ²⁶ Then, by Gödel’s second incompleteness theorem, ${\mathsf {ACA_{0}}} \nvdash {\mathsf {Con}}({\mathsf {PA}})$ . However, we do have that $\mathsf {ACA} \vdash {\mathsf {Con}}({\mathsf {PA}})$ .Footnote ²⁷ Finally, although $\mathsf {ACA}$ technically counts as infinitary, it is predicatively justified insofar as all second-order variables can be interpreted as ranging over previously defined arithmetical subsets of $\mathbb {N}$ .

In sum, Feferman has shown that GD can be challenged in its most basic form, viz., the case with which Gödel was originally concerned in [Reference Gödel, Feferman, Dawson, Kleene, Moore, Solovay and Heijenoort51]. That is, we do not require even one full iteration of the powerset on $\mathbb {N}$ in order to prove Con(PA). Rather, we can get away with $\Delta ^{1}_{1}$ -CA, and I have noted that we can get by with even less than this. Let us now turn to Feferman’s second way of undermining GD.

3 Stage II: Gödel’s Doctrine and finitary combinatorial independence results

4 Objection I: The mathematicality of independence results

We have already touched upon one of Feferman’s counterarguments in our discussion of PH: namely, the finitary combinatorial independence results lack mathematicality.Footnote ³⁷ (In what follows, I will use “artificiality” as the antonym of “mathematicality.”) He says,

and

These concerns, though somewhat “soft” and informal, should be taken seriously, at the very least because the primary impetus behind discovering PH, FKT, etc. was the presumed artificiality of Gödelian incompleteness. In order to understand and adequately respond to this counterargument, we need a better handle on what is meant by mathematicality—or lack thereof—in this context.

Let us begin by distinguishing some marks of mathematicality mentioned at various points by Barwise, Feferman, Friedman, and Simpson.Footnote ³⁸ These authors believe a statement $\tau $ possesses mathematicality provided that:Footnote ³⁹

1. (M1) $\tau $ does not involve:

   1. (a) The coding of logical syntax. (For our purposes, the most salient feature of this ban on coding is that $\tau $ does not then express a metamathematical property of a formal system, e.g., consistency).

   2. (b) Self-referentiality of any sort, even if this does not appear in coded form.Footnote ⁴⁰

2. (M2) $\tau $ arises in the course of “ordinary” mathematical work, i.e., in contexts independent of explicit metamathematical investigations.

3. (M3) $\tau $ has not been designed or “cooked up” to satisfy some further metamathematical end. In particular, $\tau $ has not been designed to demonstrate the incompleteness of a formal system.

It is clear that these authors are not providing anything like a philosophical analysis of mathematicality (whatever that might be). Rather, all they indicate is that the failure of any one of these conditions is sufficient for $\tau $ to be considered artificial in some loose, pre-philosophical sense. Each of the independence results considered by Feferman (including PH and FKT) fail more than one of these conditions, and so are deemed artificial virtually by fiat.

I think that this is far too quick, and there are subtle points to be made about each of the above conditions. Let us take them in turn. Prima facie , condition (M1) might appear quite decisive; however, the relationship between Diophantine equationsFootnote ⁴¹ and undecidable $\Pi ^{0}_{1}$ sentences complicates the picture significantly. I cannot enter into full details here, but, in short, the relationship is provided by the negative solution to Hilbert’s Tenth Problem (H10) by Matiyasevich, which itself built upon early results in computability theory by Gödel, Turing, Kleene, and many others.Footnote ⁴² From this work, it follows that each $\Pi ^{0}_{1}$ sentence is equivalent to the unsolvability of a suitable Diophantine equation, and so, in particular, undecidable $\Pi ^{0}_{1}$ sentences like the Gödel sentence G and consistency statements take such a form.

The problem, then, is this: Feferman wishes to set aside various independence results as artificial because they fail (M1). However, these statements can be expressed as Diophantine problems that involve neither the coding of logical syntax nor self-referentiality (of any sort). Even worse, Diophantine problems have long been objects of study in mathematics, and the examination of some such equations has incited the development of much mathematical research, e.g., the work flowing from Fermat’s Last Theorem. It then seems an entirely live possibility that, in studying Diophantine equations, a mathematician could be dealing with a statement that has metamathematical content without knowing that this is the case.Footnote ⁴³ What can be said about this situation? Must we accept that there is no meaningful distinction to be found here?

Here is one way to challenge the mathematicality of independence results in Diophantine form. The smallest number of variables involved in the Diophantine form of $\Pi ^{0}_{1}$ independence results is $n=9$ , although this then comes with an increase in the degrees of the polynomials in question. Going in the other direction, one can reduce the degrees of the polynomials to $d=4$ at the cost of increasing the number of variables far beyond $n=9$ [Reference Davis, Matiyasevich, Robinson and Browder16, Reference Mazur76, Reference Jones59]. Although these bounds on variables and degrees might sound rather modest, Diophantine problems found in practice typically involve significantly fewer variables (or lower degrees), and even these remain immensely difficult to solve. A nice example is the work done on the “sum of three cubes problem,” viz., whether there are integral solutions $(x,y,z)$ for $x^{3} + y^{3} + z^{3} = k$ (where k is an integer such that $k \not \equiv \pm 4\ \mod 9$ ). Indeed, only very recently has this been shown to hold for particular small values of k, viz., $33$ and $42$ [Reference Booker and Sutherland10].Footnote ⁴⁴ On the other hand, it is also known that the Riemann Hypothesis, a statement no one would wish to deny is mathematical, can be reformulated in terms of a Diophantine problem with an immense number of variables (far greater than $9$ ) [Reference Davis, Matiyasevich, Robinson and Browder16, Reference Poonen85].Footnote ⁴⁵ So, I think the appeal to the complexity of the independence results in their Diophantine form yields equivocal results at best. Perhaps what we should say is that, generally speaking, there is a difference in degree but not in kind between $\Pi ^{0}_{1}$ independence results in Diophantine form and other Diophantine equations like sums of cubes or Fermat’s Last Theorem. We might say that the latter statements are closer to the center of our “web of beliefs,” consisting of hypotheses, conjectures, axioms, and theorems, the removal of which would result in significant changes to how mathematics is done, whereas independence results in Diophantine form are closer to the “edges” of the web, and their removal would have fewer ramifications.Footnote ⁴⁶ For example, the removal of Fermat’s Last Theorem and the machinery built to prove it would result in the removal of huge and interconnected portions of algebraic geometry, number theory, and arithmetic geometry. On the other hand, the removal of $\Pi ^{0}_{1}$ independence results in Diophantine form would not result in the removal of portions of these subfields. Nor would the removal of such results even really have ramifications in areas like proof theory and computability theory, since they are not typically studied in these settings under the guise of Diophantine problems. However, we must admit that such judgements are defeasible by further evidence. This idea will be important in what follows.

Consider now (M2) and (M3). Understanding these conditions is rather difficult because they appeal to the broader aims and content of both “ordinary” mathematical work and metamathematical investigations. And these are difficult to circumscribe precisely as has already been demonstrated in the above consideration of (M1). Most salient is the fact that mathematics is full of surprising connections that take years of effort to uncover. So, just because a result might initially appear mathematically artificial given that it fails (M2) or (M3) (or both), this does not guarantee that further, countervailing evidence will not come to light. As such, it would seem that the combinatorial independence results, even if discovered in the course of metamathematical investigations and even if designed to achieve a particular metamathematical goal, could still earn their credentials of mathematicality over the course of time.

I would like to suggest that these results could do so in the following ways. Each result could:

1. (C1) Serve as an ingredient in a proof that settles a heretofore open question in mathematics.Footnote ⁴⁷

2. (C2) Serve as an ingredient in a proof of an already established result of mathematics.

3. (C3) Express an open question of mathematics.

4. (C4) Express an established result of mathematics.

5. (C5) Be obtained from a result of mathematics. This could mean: (a) the statement being tested for mathematicality is obtained by modifying the statement of an established result of mathematics in a non-ad hoc way (determined contextually) and (b) the statement being tested for mathematicality can be proved by established mathematical means, viz., without direct reference to metamathematical considerations.

My hope is that (C1)–(C5) will provide more subtle means of assessing whether our independence results enjoy some degree of mathematicality.Footnote ⁴⁸ In what follows, I will focus on (C1), (C2), and (C5).

Importantly, as an anonymous reviewer has indicated, these new conditions modify the temporality of the original conditions gleaned from Feferman et al. That is, rather than considering some $\tau $ during the brief window of time when it was “designed” to satisfy some further metamathematical end, we now consider $\tau $ in the “long run” (or, at least, “longer run”) of mathematical development. One might worry that this represents a radical departure from the original notion of mathematicality sketched by (M1)–(M3) and that, as a result, it would be open to Feferman to reject the further conditions for mathematicality. There are a few things to say about this.

First, a dialectical point: I do not think that Feferman would be unfriendly to an appeal to longer term mathematical development even if this represents a significant change in how we assess mathematicality. One reason for this is that he does not take a particularly strong position on whether, say, the fact that some $\tau $ fails (M3) determines that $\tau $ is artificial for all time. He simply positions himself at a particular juncture in mathematical development and assesses results from this perspective. Another reason is that Feferman adopts a “long term” attitude towards the assessment of GD throughout the discussion of [Reference Feferman28] and does appear to leave it open as to whether further evidence for, say, the mathematicality of Diophantine independence results might materialize.

Second, when we are attempting philosophical explications of informal or vague concepts present in mathematical research, e.g., mathematicality, fruitfulness, naturalness, understanding, etc., an appeal to the history of mathematics is essential for making any progress. A careful consideration of this historical development can provide the material for giving more objective content to these informal concepts (or show that more objective articulation is unlikely to materialize). Suffice it to say, I am hopeful that this way of proceeding can yield real philosophical insight into mathematics. To mention one exemplary case, Tappenden has convincingly argued that the definition of the Legendre symbol in number theory, though “unnatural” or “gerrymandered” by typical metaphysical standards of disjunctiveness, is in fact “natural” insofar as it is a special case of a more general and fundamental concept, the Artin symbol. However, in making this claim, Tappenden relies on approximately 200 years of number-theoretic research culminating in the Artin Reciprocity Theorem [Reference Tappenden and Mancosu100].Footnote ⁴⁹ Indeed, my proposal for determining mathematicality via the resolution of conjectures and inductive success coheres nicely with the discussion of mathematical naturalness in [Reference Tappenden and Mancosu100]. Tappenden emphasizes that judgments of naturalness cannot be determined by flatfootedly appealing to the context in which the statement occurs. Rather, the judgment that a definition, property, theorem, etc. is natural often requires the accumulation of evidence over long periods of time. Similarly, I am stressing that we should play a longer game in assessing the mathematicality of the independence results. That is, if we can show that our independence results are not merely isolated pieces of metamathematical work, but rather satisfy (C1) and/or (C2), viz., they are fruitful in mathematical practice, then we have (defeasible) evidence for their mathematicality.

Let us now apply these ideas to the independence results. I have already noted some ways in which we might construe PH as mathematically artificial.Footnote ⁵⁰ On the other hand, there is evidence that FKT is much less so.

It is best to start with KTT of which FKT is a finitary miniaturization. The former is a well-known and powerful result from “ordinary” mathematics. It addresses a readily comprehensible question about embeddability properties of trees. There is nothing in its statement smacking of metamathematical notions or of the coding of syntax. Furthermore, it has proved to be a fundamental result in combinatorics and theoretical computer science insofar as it is used to show that various orderings on trees are well-founded.Footnote ⁵¹ Thus, KTT is evidently mathematical.

But what of FKT? It fails (M2) and (M3) above, and so, by Feferman’s lights, is mathematically artificial. In particular, apropos (M3), one might have the following worry: when we modify KTT to get FKT, is this modification explicitly designed to mirror some feature of the ordinal representation system in order to generate independence? That is, although KTT seems eminently mathematical, FKT might not be if it has been so designed.

First, note that the independence proofs for both KTT and FKT proceed in virtually the same way, and one is not inclined to think that KTT is “artificial” given the relationship between tree embeddings and ordinal representations. Thus, one should not necessarily be worried about FKT. We must, however, examine more carefully how FKT is produced from KTT, since this procedure could be highly contrived.

Consider the following line of thought: we look at KTT and wish to provide a finitization of it. It seems eminently reasonable first to consider a sequence of trees with an initial restriction on tree size. Then, stipulate the simplest possible (nontrivial) growth rate on the size of the trees, viz., a linear growth rate. Finally, ensure that the sequence of trees is finite by providing a bound n depending on k which gives the position in the original (infinite) sequence of trees where some $T_{i} \boldsymbol {\leq }_{e} T_{j}$ for $i<j \leq n$ .Footnote ⁵² And, voilà , this does the trick! As one can see, there is no complicated finagling of the original result: FKT arises from KTT without questionable or ad hoc or even particularly difficult hypotheses. Nor does the finitization procedure require that we draw from any properties of the ordinal representation system used in the independence proof. Indeed, it seems that the similarity in independence proofs is a symptom of a deeper fact, viz., FKT and KTT are very similar in terms of their mathematical content. Hence, since we agree that KTT is mathematical, so too is FKT (using C5).

Finally, it is worth noting that in order to prove FKT independent from ${\mathsf {ATR_{0}}}$ , the primitive recursive ordinal representation system is modified to accommodate the statement of FKT, not the other way round [Reference Simpson, Harrington, Morley, Scedrov and Simpson94, p. 101]. This is significant because we will see below that the opposite is done for other independence results. Hence, the conceptual flow of Friedman’s proof is as follows: begin with the mathematical statement KTT; produce FKT directly from KTT using an entirely non-ad hoc finitization procedure; then alter a given ordinal representation system to mirror the statement of FKT; and finally, prove the independence of FKT.Footnote ⁵³ Thus, given the direct way in which FKT is obtained from KTT, the accommodation of ordinal representations to FKT itself, and the favorable comparison to PH, we have some reasonable grounds for thinking FKT is mathematical. However, FKT is really just the beginning of a fascinating story involving “Kruskal-like” theorems, and it is these further theorems that are more consequential for our purposes given their fruitfulness.

4.1 Extended Kruskal’s Theorem (EKT) and its finite variant

Shortly after establishing the independence results for KTT and FKT, Friedman devised an “extended” form of KTT, typically called Extended Kruskal’s Theorem, which we denote by EKT. The statement of EKT is obtained from KTT by imposing a “Gap Condition” on the tree embedding used.

Definition 4.1. For $n < \omega $ , let $\mathscr {T}_{n}$ be the set of all finite trees assigned labels from n, i.e., $(T, \ell ) \in \mathscr {T}_{n}$ iff $T \in \mathscr {T}$ (see Remark 3.6) and $\ell : T \rightarrow \left \{0, 1, \ldots , n-1\right \}$ is a labelling function. We then say that $(\mathscr {T}_{n}, \boldsymbol {\leq }_{e})$ is a quasiordering iff there is an embedding $f: (T_{1}, \ell _{1}) \rightarrow (T_{2}, \ell _{2})$ such that:

1. 1. (Label stability) For each $b \in T_{1}$ , we have $\ell _{1}(b)=\ell _{2}(f(b))$ .

2. 2. (Gap condition) If b is an immediate successor of $a \in T_{1}$ , then for each $c \in T_{2}$ satisfying $f(a) < c < f(b)$ , we have that $\ell _{2}(c) \geq \ell _{2}(f(b))$ .

We then have the following theorem.

Theorem 4.2 (Extended Kruskal’s Theorem; $\mathsf {EKT}$ )

For each $n < \omega $ , $(\mathscr {T}_{n}, \boldsymbol {\leq }_{e})$ is a well-quasiordering. In other words, there is no infinite set of pairwise non-embeddable finite labelled trees, where our embedding satisfies the two conditions in Definition 4.1.

Once more, we can “finitely miniaturize” EKT to produce the finite variant, Extended Finite Kruskal’s Theorem (EFKT). This process is exactly like the one used to produce FKT from KTT, and so it is similarly direct. Friedman then showed the following theorem ([Reference Simpson, Harrington, Morley, Scedrov and Simpson94, pp. 113–114] and [Reference Friedman, Robertson, Seymour and Simpson45]).

Theorem 4.3. Neither EKT nor EFKT is provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ . However, each is provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}}$ .

This is all really quite surprising, since, from the perspective of ordinary mathematical practice, ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ is very strong. We have seen that it is an expressly impredicative subsystem of ${\mathsf {PA}}_{2}$ , and thus, according to Feferman, requires that the full power-set $\mathscr {P}(\mathbb {N})$ exists as a “fixed” totality. Furthermore, ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ suffices to prove central results of classical descriptive set theory, the structure theory of countable abelian groups, and the famous Cantor–Bendixson theorem, all of which are beyond the reach of ${\mathsf {ACA_{0}}}$ and even of ${\mathsf {ATR_{0}}}$ .

The proof of Theorem 4.3 is rather more complicated than that of the corresponding result for KTT (Theorem 3.8) in part because a new ordinal notation system is required to express the proof-theoretic ordinal of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ .Footnote ⁵⁴ With this in hand, however, the proof strategy is similar to that of Theorem 3.8: we show that EKT implies the well-foundedness of the proof-theoretic ordinal of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ , written as $\psi _{0}(\Omega _{\omega })$ (in the ordinal representation system of [Reference Buchholz11] used by [Reference Simpson, Harrington, Morley, Scedrov and Simpson94]), where this implication is itself provable in ${\mathsf {ACA_{0}}}$ . However, the well-foundedness of $\psi _{0}(\Omega _{\omega })$ is not provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ . Hence, EKT is not provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ . One then proceeds in analogous fashion for the finite version.

One can see that the additional power needed to prove EKT and EFKT (relative to the proofs of KTT and FKT) derives from the imposition of the “Gap Condition” on the embedding $f: T_{1} \rightarrow T_{2}$ . So, the question becomes: what is the origin of the Gap Condition? Was this simply “cooked up” by Friedman in order to yield the desired independence result? Or did it arise in the course of ordinary combinatorial work?

Unfortunately, a closer look at the independence proof for EKT does in fact support Feferman’s allegations of artificiality. Start with the ordinal representation system of [Reference Buchholz11], which yields $\psi _{0}(\Omega _{\omega })$ as the proof-theoretic ordinal of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ , and consider the terms (in the ordinal representation system) as representing labelled trees and subtrees. One quickly finds that, in order to get the term representing $T_{1}$ to be less than the term representing $T_{2}$ , viz., $\tau (T_{1}) \leq \tau (T_{2})$ , one requires precisely the Gap Condition on $f: T_{1} \rightarrow T_{2}$ .Footnote ⁵⁵ That is, if $T_{1}$ is gap-embeddable in $T_{2}$ under f, i.e., $T_{1} \boldsymbol {\leq }_{e} T_{2}$ , then $\tau (T_{1}) \leq \tau (T_{2})$ in the ordinal representation system for the proof-theoretic ordinal of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ . From this, it is shown that

(9) $$ \begin{align} (\forall n < \omega)(\mathscr{T}_{n} \ \text{is a well-quasiordering} \rightarrow \mathsf{WO}(\psi_{0}(\Omega_{\omega})), \end{align} $$

where the implication is provable in ${\mathsf {ACA_{0}}}$ . Finally, since ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}} \nvdash \mathsf {WO}(\psi _{0}(\Omega _{\omega }))$ , we conclude that EKT is not provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ .

This is all grist for Feferman’s mill: EKT (and hence EFKT) fails (M2) and (M3) given that the Gap Condition was imposed expressly to generate the desired independence result. This is quite different from the independence proof for FKT, and the comparison is instructive. We have precisely the opposite conceptual flow as in the case of FKT where the statement of the theorem itself is accommodated by the ordinal notation system. And so, FKT continues to look quite natural, whereas EKT and EFKT look quite artificial.

4.2 EKT, the graph minor theorem (GMT), and more finite variants

In spite of all this, there is a strong argument to be made for the mathematicality of EKT on the basis of its fruitfulness in ordinary mathematical practice.Footnote ⁵⁶ In particular, EKT has been used at a crucial juncture of the proof of the monumental graph minor theorem (GMT), established over the course of 25 years and 20 substantial papers by Robertson and Seymour (see [Reference Robertson and Seymour88] for the concluding paper in the series). GMT is one of the most important theorems of graph theory and resolves two long-standing conjectures of Vázsonyi and Wagner, respectively. Furthermore, many of the techniques developed to prove GMT have led to “entirely new concepts and a new way of looking at graph theory” [Reference Lovász69]. This provides serious evidence that EKT, though by all appearances artificial and contrived (especially because of the Gap Condition), is in fact mathematical and perhaps even “natural” in a more robust sense. Finally, one can then try to reason to the mathematicality of EFKT from EKT. The reasoning is, in essence, the same as that present in the transition from KTT to FKT. Thus, we have an argument, via (C1) and (C5) above, for the mathematicality of EFKT. And so, we can say that we have a finitary, reasonably “mathematical” statement whose proof requires impredicative resources. Thus, GD may still be thought to hold.

If one is unconvinced by such a line of argument, I believe the following considerations are more decisive. Let us begin with GMT itself. We require a few brief preliminary definitions.Footnote ⁵⁷

Definition 4.4 (Graph)

A graph G is a pair of sets $G= (V, E)$ such that $E \subseteq [V]^{2}$ , i.e., the elements of E are $2$ -element subsets of V. V is called the vertex-set of G, and E is called the edge-set of G. Furthermore, an incidence relation is defined between V and E. We say that a vertex $v \in V$ is incident with edge e if $v \in e$ . Edges are either loops with one incident vertex or links with precisely two incident vertices. Incident vertices are often called the endvertices of an edge, and these endvertices are said to be adjacent in G.

Definition 4.5 (Graph isomorphism)

Let $G_{1}=(V_{1}, E_{1})$ and $G_{2}=(V_{2}, E_{2})$ be two graphs. Then we say that $G_{1}$ and $G_{2}$ are isomorphic, written as $G_{1} \simeq G_{2}$ , if there is a pair of bijective maps $f_{v} : V_{1} \rightarrow V_{2}$ and $f_{e} : E_{1} \rightarrow E_{2}$ that preserve the incidence relation. We write $f=(f_{v}, f_{e})$ to denote the graph isomorphism.

Definition 4.6 (Graph minor)

Any graph $G^{\prime }$ produced from a given G by successive applications of the following reduction operations (in any order) is said to be a minor of G. The reduction operations are: (i) edge deletion; (ii) edge contraction; and (iii) isolated vertex deletion. Furthermore, every graph that is isomorphic to a minor of G is also called a minor of G. (See [Reference Friedman, Robertson, Seymour and Simpson45, p. 234] for a more formal definition).

With these definitions in hand, we can now state the GMT. There are a number of equivalent ways of doing so. I will use the language of well-quasiorderings so as to make the connection to the above independence results clearer. Note that graphs are finite, undirected, and may have loops or multiple edges.

Theorem 4.7 (GMT; Robertson and Seymour)

For any infinite sequence of finite graphs $\langle G_{n}: n < \omega \rangle $ , there exist $i,j$ with $i<j$ such that $G_{i}$ is isomorphic to a minor of $G_{j}$ . In other words, let $\mathscr {G}$ be the set of (isomorphism classes) of finite graphs and let $\boldsymbol {\leq }_{m}$ be the minor relation. Then $(\mathscr {G}, \boldsymbol {\leq }_{m})$ is a well-quasiordering.

As indicated above, even a cursory discussion of the proof of this theorem and its connections to other areas of graph theory is far beyond the scope of this paper (or, more generally, of any one paper). It suffices to quote Diestel on this:

Our goal in this last chapter 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. This graph 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. $[\ldots $ ] [A]s with most truly fundamental results, the proof has sparked off the development of methods of quite independent interest and potential. This is true particularly for the use of tree-decompositions, a concept that is not only central to graph minor theory but has found algorithmic applications too, and tangles a radically new notion of high connectivity somewhere inside a given graph. [Reference Diestel18, p. 347]

Fortunately, the steps of the proof of GMT that invoke infinitarily strong resources, viz., EKT, are readily identifiable. In an early paper of the “Graph Minors” series, Robertson and Seymour seek to prove a special case of GMT, which they call the “Bounded GMT” (BGMT) [Reference Robertson and Seymour87]. In particular, they aim to show that $(\mathscr {B}, \boldsymbol {\leq }_{m})$ , where $\mathscr {B}$ is the class of finite graphs with bounded tree-width, is a well-quasiordering. In the broadest strokes, when a graph G has “bounded tree-width” p, one is able to build G up uniformly in stages from subgraphs enjoying nice topological properties.Footnote ⁵⁸ One then applies a modified version of EKT to this hierarchy of decompositions.

Of course, it is natural to wonder whether this application of EKT is avoidable. It turns out that the answer is “no.” In particular, Friedman et al. [Reference Friedman, Robertson, Seymour and Simpson45, secs. 3–4] show that one can derive EKT from BGMT, thereby establishing the following theorem.

Theorem 4.8. Over ${\mathsf {RCA_{0}}}$ ,Footnote ⁵⁹ we have the following equivalence:

(10) $$ \begin{align} {\mathsf{BGMT}} \Longleftrightarrow {\mathsf{EKT}}. \end{align} $$

Thus, BGMT is provable in $\mathsf {\Pi ^{1}_{1}}$ -CA but not in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ .

Thus, by Feferman’s lights, we now have a theorem of acknowledged “mathematicality” (insofar as it satisfies conditions (M1)–(M3) above) that necessarily requires impredicative resources for its proof. We do not yet have support for GD, though, since BGMT quantifies over infinite sequences of finite graphs of bounded tree-width $\langle B_{n} : n < \omega \rangle $ . However, as with the infinitary KTT and EKT, we can “finitely miniaturize” BGMT in precisely the same fashion to produce the following theorem.

Theorem 4.9 (Finitary BGMT; Friedman)

For all $k,p$ , there is an n such that for any finite sequence of finite graphs $\langle G_{1}, \ldots , G_{n} \rangle $ of bounded tree-width $\leq p$ and satisfying $|G_{i}| \leq k+i$ for all $i \leq n$ , then there exist indices $i,j$ such that $i < j \leq n$ and $G_{i} \boldsymbol {\leq }_{m} G_{j}$ . (Note that $|G_{i}|$ denotes the sum of the number of vertices and number of edges of graph $G_{i}$ ).

Finally, Friedman shows the following theorem.Footnote ⁶⁰

Theorem 4.10. Finitary BGMT is provable in $\mathsf {\Pi ^{1}_{1}}$ -CA but not in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ .

Thus, we have a finitary theorem of acknowledged “mathematicality” that necessarily requires impredicative resources for its proof. And hence, we have a significant counter-example to Feferman’s arguments against the finitary independence results. GD remains intact.Footnote ⁶¹

5 Objection II: 1-consistency versus set existence

Feferman’s second objection is related to his argument (surveyed in §2.3) that we can replace GD with less metaphysically weighty variants that nonetheless prove the finitary statements of interest. The objection is very briefly stated and merits closer inspection:

The basic idea is as follows: each of our finitary independence results is shown to be independent of a given subsystem by proving that each statement implies or is equivalent to the 1-consistency of the subsystem. So, Feferman’s suggestion is that we simply assume such 1-consistency statements, which are themselves arithmetical (in particular, $\Pi ^{0}_{2}$ ), in order to derive our independence results. As with his truth-theoretic and reflection principle variants discussed in §2.3, this allows us to avoid platonistic commitment to impredicative set-existence principles. However, I believe that Feferman runs into trouble here because he has, seemingly, no principled reason to accept such 1-consistency statements.Footnote ⁶⁶

Consider finitary BGMT. This is a theorem of acknowledged mathematicality, proved by ordinary mathematical means. Over a particular weak system of arithmetic, this is equivalent to $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ .Footnote ⁶⁷ So, according to Feferman, what is really necessary here for the derivation of finitary BGMT is not $\mathsf {\Pi ^{1}_{1}}$ -CA but only $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ (cf. Theorem 4.10). But why accept $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ as true? It seems Feferman must do so given its equivalence with an acknowledged theorem of ordinary mathematics; elsewhere, after his brief acknowledgement of the mathematicality of FKT and EFKT (see fn. 37), he favorably compares these results to other finitary statements due to Friedman, saying

That is, whereas these $\varphi $ are only accepted if we accept certain 1-consistency statements, precisely the opposite happens for FKT and EFKT. We prove these without appeal to 1-consistency statements, find that they are equivalent to such statements, and so, by dint of our acceptance of FKT and EFKT, we accept the 1-consistency statements. The favorable comparison is even clearer for finitary BGMT as there is no question of its mathematicality.

But now Feferman is trying to proceed in the other direction from 1-consistency statements to finitary combinatorial theorems. The question then becomes: can he provide independent reasons for accepting the relevant 1-consistency statements as true? If so, then he can proceed from the truth of such statements to the truth of our finitary combinatorial independence results. Unfortunately, I cannot see how he might do this, especially in light of the deflationary moves from §2.3. Indeed, Feferman cannot accept the “correctness” of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ as this is an impredicative subsystem, and so he cannot leverage this acceptance into the further acceptance of ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ , $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ , etc. In fact, he has made his situation worse: by invoking the equivalence between finitary BGMT and $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ , he is now responsible for making sense of the truth of a new finitary metamathematical statement! His final objection against GD can be employed to provide principled acceptance of $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ (and other such statements), but this will in fact enable us to turn other epistemic considerations against him.Footnote ⁶⁸

Thus, in the next two sections, I will consider Feferman’s final objection and then ascertain the epistemic costs that must be weighed against his anti-platonist program. In particular, I believe that Feferman’s program leaves us with (i) less than satisfactory proofs of individual results; and (ii) a less than satisfactory account of the interplay between metamathematics and mathematics, viz., a loss of global explanatory structure. I will then show how these considerations can be used to argue for my restricted and epistemic version of GD.

6 Objection III: Proof-theoretic reductions

Feferman’s third and final objection appeals to proof-theoretic reductions of subsystems of ${\mathsf {PA}}_{2}$ to constructive theories. The basic idea is that, if we can proof-theoretically reduce, say, the impredicative theory ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ to some weaker theory, which is itself justified without appeal to ${\mathscr {P}}(\mathbb {N})$ , then the use of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ in the finitary independence results is anodyne.Footnote ⁶⁹ The results contained in [Reference Buchholz, Feferman, Pohlers and Sieg12] provide examples of such reductions in terms of “iterated inductive definitions.” In particular, it is shown that ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ is (finitarily) reducible to ${\mathsf {ID}^{i}_{<\omega }} := \bigcup _{n< \omega } \mathsf {ID}^{i}_{n}$ with respect to $\Pi ^{0}_{2}$ formulas. Here ${\mathsf {ID}^{i}_{<\omega }}$ is a constructive (i.e., intuitionistic, indicated by the i superscript) system of inductive definitions iterated $< \omega $ times. To fix intuitions, let me briefly define the simplest theory of iterated inductive definitions, ${\mathsf {ID}_{1}}$ , first introduced by Kreisel.Footnote ⁷⁰ Note that this theory is not intuitionistic.

Example 6.1. ${\mathsf {ID}_{1}}$ is an axiomatic theory consisting of the axioms of PA with additional predicates P defined in the following way. Take some arithmetical formula $\varphi (P, x),$ where P has only “positive occurrences” in $\varphi $ . The positivity condition means that P always occurs without negations when we write everything in negation-normal form. This ensures that we get “new information” only from “previously given information” or “from below.” This is quite important as Feferman relies on this kind of intuitive gloss in defending iterated inductive systems as especially perspicuous. Given the positivity constraint, we can then define a monotonic operator:Footnote ⁷¹

(11) $$ \begin{align} \Gamma_{\varphi}: {\mathscr{P}}(\mathbb{N}) \rightarrow {\mathscr{P}}(\mathbb{N}), \quad \Gamma_{\varphi}(X)= \left\{ x \in \mathbb{N} : \varphi(X, x) \right\}. \end{align} $$

The monotonicity of $\Gamma _{\varphi }$ is sufficient to show that there is a smallest fixed point, $I_{\Gamma _{\varphi }} := \bigcap \left \{ X: \Gamma _{\varphi }(X) \subseteq X \right \}$ . The new predicates P for ${\mathsf {ID}_{1}}$ are then just such smallest fixed points associated with each formula $\varphi $ . We complete the construction of ${\mathsf {ID}_{1}}$ by adding the following axioms:

1. 1. $\forall x (\varphi (P, x) \rightarrow P(x))$ ;

2. 2. $\forall x(\varphi (\psi _{P}, x) \rightarrow \psi (x)) \rightarrow \forall x (P(x) \rightarrow \psi (x))$ ,

for each $\psi $ and where $\psi _{P}$ means that we replace atomic formulas P with $\psi $ .

Given the availability of the proof-theoretic reduction of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ to ${\mathsf {ID}^{i}_{<\omega }}$ , Feferman believes we can dispense with the problematic impredicative principles. Indeed, in light of this reduction, we are supposed to be in a very ontologically secure place for two reasons. First, we utilize only intuitionistic logic in ${\mathsf {ID}^{i}_{<\omega }}$ and thus do not appeal to the “completed infinite.” Second, ${\mathsf {ID}^{i}_{<\omega }}$ employs only countable sets generated from very concrete, previously obtained, information. Thus, we are to conclude that

Hence, according to Feferman, even if one believes that the independence results discussed above are reasonably mathematical, and even if one finds the use of 1-consistency statements unprincipled, the availability of these constructive reductions still undermines GD.

I can now flesh out my two final objections to Feferman’s argument. The first will address the relationship between constructive reductions of subsystems of ${\mathsf {PA}}_{2}$ and proofs of our independence results in these systems. The second will apply both to this point and to the foregoing maneuver concerning $1$ -consistency.

7 Unification and explanation

Fittingly, my final response to Feferman’s last two objections derives from Gödel’s distinctive views concerning the justification of axioms. Consider the following famous passage:

Concerning (a): I have already argued for the verificational role of infinitary resources in the preceding section. It is highly plausible that, at the very least, the proofs of the finitary relatives of GMT utilizing ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}}$ will be much easier to verify than proofs carried out in constructive theories of iterated inductive definitions. This is likely also the case for FKT and EFKT, although the difference in proofs will be less dramatic. Thus, these are particular cases that lend weight to Gödel’s claim that proofs using particular axioms will be “simpler.” It is hard to say much about “discovery,” given that we are entirely at the mercy of the history of mathematics here, but, of course, all our results were in fact discovered using strong infinitary resources and not 1-consistency statements or constructive reductions. Let us now flesh out Gödel’s ideas in (b) to bolster further our case against Feferman.

Consider our situation at this juncture. We have an interesting collection of suitably mathematical, finitary statements (FKT, EFKT, and the finitary relatives of GMT), all of which are provably independent of particular subsystems of ${\mathsf {PA}}_{2}$ $({\mathsf {ATR_{0}}}$ for FKT, ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ for EFKT and finitary BGMT, and $\mathsf {\Pi }^{1}_{1}$ -CA for finitary GMT). As Feferman has argued, all we really need is the 1-consistency of the relevant subsystems to obtain our finitary statements, and so we do not need any of the metaphysically suspect set theory. However, I noted that this move is rather puzzling given that Feferman cannot recognize, e.g., ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ as “informally correct,” and so has no grounds for thinking, e.g., $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ is true. But now the proof-theoretic reductions of our subsystems to constructive theories of iterated inductive definitions provide such grounds. Hence, Feferman’s final objection transforms the combinatorial independence results and the relevant 1-consistency statements into “verifiable consequences” of the set-theoretic comprehension schemata governing our subsystems, i.e., consequences demonstrable without such set-theoretic principles. And thus, Gödel’s considerations above become an eminently reasonable response to Feferman.

But what, exactly, do these considerations amount to? I think the most forceful elaboration will make use of a notion of explanation, and I believe this is what Gödel himself had in mind. In particular, a “global” conception of explanation in mathematics, viz., a conception in which explanatory power is construed as a property of theories, frameworks, or axiomatic systems (rather than of proofs), is present in many works by those in the “h-inductivist” tradition [Reference Mancosu72].Footnote ⁷⁶ This is quite explicit in some (Russell and Lakatos), but only implicit in others, including Gödel.

However, interpreting Gödel’s quote in terms of explanation is supported (as noted in [Reference Mancosu72]) by the report of a conversation between Mehlberg and Gödel:

Gödel’s suggestion that postulates in physics and “foundations” in mathematics both serve as explanatory hypotheses confirms that sentence (b) above should be understood in terms of explanation, especially given its reference to “well-established physical theory.”Footnote ⁷⁷

But what sort of explanation might Gödel have had in mind? What sort fits the situation of the finitary independence results? Although the topic of mathematical explanation has gained a good deal of attention in recent years, little work has been done on developing models for a “global” conception of explanation as opposed to a “local” conception (in the latter, explanatory power is considered a property of proofs) [Reference Mancosu, Poggiolesi, Pincock, Zalta and Nodelman74, Reference Pincock84]. Nonetheless, the exemplar of such a global conception, Philip Kitcher’s “unificationist” approach, finds some purchase in our situation [Reference Kitcher63, Reference Kitcher, Kitcher and Salmon64].

In broad strokes, Kitcher’s view is as follows. We consider first the set K of beliefs (assumed consistent and deductively closed) of an idealized scientific/mathematical community at a given moment in time. We then proceed to examine possible systematizations of K, where a systematization is a set of derivations, which derive particular sentences in K from other sentences in $K^{*}$ , where $K^{*}$ is a consistent superset of K which can be rationally accepted by those who accept K.Footnote ⁷⁸ Then, a given derivation will count as explanatory if it belongs to the “explanatory store” over K, $E(K)$ , which is the systematization that scores best according to the following three criteria: minimization of “argument patterns,” the maximization of conclusions, and the “stringency” of argument patterns.Footnote ^{79 ,} Footnote ⁸⁰

Despite the sophistication of the model, recent work has shown that its precise details fail to make good sense of explanatory judgments in mathematical practice [Reference Hafner, Mancosu and Mancosu54]; however, the idea that explanation and unification are intimately related is pervasive in both mathematics and the sciences, and I believe the most basic insights of Kitcher’s model can still be fruitfully applied to our case. In general, I doubt that any single model of explanation will suffice to capture the complexity of this notion. My intent in what follows is simply to put more flesh on the bones of Gödel’s sketchy remarks, and Kitcher’s account serves this purpose well.

Consider: we begin with a collection of reasonably mathematical, finitary independence results and their 1-consistency equivalents (or consequences).Footnote ⁸¹ These can be proved using appropriately strong subsystems of ${\mathsf {PA}}_{2}$ . However, as Feferman argues, another route is available: use instead the constructive reductions of these subsystems. Thus, by appeal to these reductions, our independence results are now transformed into “verifiable consequences” in Gödel’s sense. Now we ask for what best explains, i.e., best unifies, this disparate collection of verifiable consequences, the subsystems based upon set-theoretic comprehension principles or the constructive reductions.

A reasonable proposal for the best explanation (in our sense) would be: the optimalFootnote ⁸² subsystem of ${\mathsf {PA}}_{2}$ that can prove each statement in our collection of verifiable consequences. Schematically, presented with $1$ - ${\mathsf {Con}}(S)$ , the strongest of the consistency statements in our collection, we select the optimal $S^{\prime }$ proof-theoretically stronger than S, written as $S^{\prime }> S$ , that will prove $1$ - ${\mathsf {Con}}(S)$ and its equivalent statements.Footnote ⁸³ This move coheres nicely with Kitcher’s basic picture because a single “argument pattern” allows us to derive many independently verifiable results (and other results besides). Furthermore, this move satisfies a kind of “stringency” requirement given that we do not allow just any sufficiently strong axiomatic system be employed, e.g., ${\mathsf {PA}}_{2}$ , ZFC, or beyond. We are guided by the S appearing in the relevant $1$ - ${\mathsf {Con}}(S)$ to make our choice. This makes our pattern of argument more difficult to instantiate, and hence avoids trivializing the unification. So, what should $S^{\prime }$ be in our case?

Before answering this, there is one small issue to note: I would like to capture as verifiable consequences two finitary versions of GMT that I have not explicitly discussed. These are known to be independent of ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}}$ , to imply (over a suitable weak subsystem) $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA_{0}}})$ , and to be provable in ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}} + \mathsf {BI}$ , where $\mathsf {BI}$ is the principle of Bar Induction, which says that one can carry out transfinite induction along any well-founded ordering [Reference Friedman, Robertson, Seymour and Simpson45, theorem 5.1]. However, no interesting equivalence with a 1-consistency statement, e.g., $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}})$ , is known. Presumably, such a 1-consistency statement could be found, given that all our finitary statements are $\Pi ^{0}_{2}$ and all others besides the finitary GMT have been shown to have such equivalences. Let us assume that $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}})$ will do the trick. If this is incorrect, my argument here can be easily modified to accommodate the correct equivalence.Footnote ⁸⁴ Thus, given our verifiable consequences, we may conclude that ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}} + \mathsf {BI}$ is needed.

However, Feferman seems to have a number of ready responses to this move. First, he could once more say that we do not need ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}} + \mathsf {BI}$ but only, say, $1$ - ${\mathsf {Con}}({\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}})$ . But this once more runs into my objection about 1-consistency statements: why think such statements are true when they are statements about sufficiently strong systems? Feferman can then retreat as follows. Since we have selected the optimal subsystem needed for this unification, ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}} + \mathsf {BI}$ , and since this subsystem is not yet beyond the reach of proof-theoretic reductions to systems of intuitionistic iterated inductive definitions, we can simply use the relevant reduction (preserving $\Pi ^{0}_{2}$ sentences). In this case, it would be the system $\mathsf {ID}^{i}_{\omega }$ [Reference Buchholz, Feferman, Pohlers and Sieg12].

Once more, Kitcher’s unificationist account helps us to deal with Feferman’s objections. Note that these reductions are, in this setting, conceptually parasitic on the classical subsystems, and this results in a proliferation of argument patterns. This is because Feferman proposes that we use $\mathsf {ID}^{i}_{\omega }$ to prove each $\Pi ^{0}_{2}$ statement in our collection rather than ${\mathsf {\Pi ^{1}_{1}}{-}\mathsf {CA}} + \mathsf {BI}$ . But the identification of this reduction as the appropriate one relies on our first, “classical” argument pattern: presented with $1$ - ${\mathsf {Con}}(S)$ , we use S to identify the relevant $S^{\prime }$ , and then derive each of our desired consequences in $S^{\prime }$ . Feferman’s objection does this and then adds the further argument pattern: given $S^{\prime }$ (identified from the above), find the relevant system $S^{\prime \prime }$ of intuitionistic iterated inductions preserving $\Pi ^{0}_{2}$ statements, and then derive each consequence in $S^{\prime \prime }$ . On this approach, no new consequences are gained, and argument patterns are not minimized. Thus, according to the basic insights of Gödel and to our unificationist model of explanation, the use of strong, impredicative subsystems best explains our finitary results.Footnote ⁸⁵

A natural objection would be to point out that the argument of the last paragraph assumes that we can individuate argument patterns (and their instantiations) without difficulty. Call our “classical” argument pattern $\pi _{c}$ and our “reductionistic” argument pattern $\pi _{r}$ . To a first approximation, on Kitcher’s view, we would like to compare the relative explanatory power of systematizations $\Sigma _{1}$ and $\Sigma _{2}$ of K, our set of arithmetical/finitary theorems. In this case, we have basis $B_{1}$ for $\Sigma _{1}$ containing $\pi _{c}$ and other argument patterns for other finitary theorems and basis $B_{2}$ for $\Sigma _{2}$ containing both $\pi _{c}$ and $\pi _{r}$ (and other patterns). Accordingly, $B_{2}$ fares worse along the dimension of argument pattern minimization. However, it seems entirely licit for Feferman to conjoin argument patterns $\pi _{c}$ and $\pi _{r}$ into a single argument pattern $\pi _{f}$ :

1. 1. Select the strongest $1$ - ${\mathsf {Con}}(S)$ from our set of verifiable consequences.

2. 2. Select the optimal $S^{\prime }> S$ that proves $1$ - ${\mathsf {Con}}(S)$ .

3. 3. Find the relevant reduction $S^{\prime \prime }$ for $S^{\prime }$ .

4. 4. Prove a conservativity result for relevant sentences.

5. 5. Derive verifiable consequences $\varphi $ .

But then $B_{2}$ contains only $\pi _{f}$ , $B_{1}$ contains only $\pi _{c}$ , and so $\Sigma _{1}$ and $\Sigma _{2}$ will be judged to have the same unificatory, and hence explanatory, power.

This kind of “conjunctive” issue is one that has plagued many unificationist accounts of explanation.Footnote ⁸⁶ A way to approach this issue would be to stipulate that derivations should not contain redundant or “idle” premises.Footnote ⁸⁷ In our case, we simply note that the explananda in question, i.e., the subset of K consisting of our finitary verifiable consequences $\varphi $ , can be derived using $\pi _{c}$ alone, and so the addition of the steps from $\pi _{r}$ is unnecessary. However, it then looks as though the proponent of the reductionist approach could re-write $\pi _{r}$ so as to include no specific dependence on the $S^{\prime }$ appearing in $\pi _{c}$ . This would amount to determining the system of iterated inductive definitions required to prove our verifiable consequences and doing so independent of appeal to any classical subsystems. But this seems quite difficult given our present state of knowledge. Consider: given one of our $1$ - ${\mathsf {Con}}(S)$ statements or one of our combinatorial theorems, how would one go about locating the relevant system? This is easy if one is allowed to appeal to the instantiation of S in a $1$ - ${\mathsf {Con}}(S)$ statement (as in $\pi _{c}$ above), but otherwise one would be proceeding quite blindly. In short, given our current knowledge, the use of iterated inductive definitions to prove our statements makes some appeal to the classical subsystems. Perhaps this is a weak conclusion; it is a conceptual possibility that one of our verifiable consequences could have been proved in, say, $\mathsf {ID}^{i}_{\omega }$ , from the start, but since the combinatorial theorems at least arise from classical mathematics, some conceptual connection would have to be provided. These considerations cut against a direct reductionist derivation that makes no reference to $\pi _{c}$ .

So, I think the classical strategy remains more parsimonious in its use of argument patterns. However, even if one disagrees, there is a final conclusive point to be made. The K we are seeking to systematize includes not just the independence results that have been our focus but all finitary/arithmetical theorems. And, although we have conservation results for systems of intuitionistic iterated inductive definitions, only $\Pi ^{0}_{2}$ sentences are conserved and not all arithmetical statements.Footnote ⁸⁸ Hence, even if we bite the bullet on the number of argument patterns, the systematization of K that uses the classical pattern $\pi _{c}$ will prove more relevant theorems. And so, the use of impredicative subsystems best unifies (and hence explains) finitary mathematics, which has been our ultimate focus.