# In what sense is the “descending chain principle” for ordinals less than $\epsilon_0$ 'infinitary?

In the introduction to his paper "Assignment of Ordinals to Terms for Primitive Recursive Functionals of Finite Type", W.A. Howard writes:

Gentzen...showed that the consistency of first order (classical or intuitionistic ) arithmetic can be proved by methods which are finitary except for the use of the descending chain principle for the ordinals less than $\epsilon_0$.

In their paper, "Goedel's Function ("Dialectica") Interpretation", Avigad and Feferman have this to say about Howard's paper:

For terms of $\mathrm T$, this task [the task of assigning ordinals (or notations representing ordinals) to terms in such a way that each one-step reduction leads to a decrease in the associated ordinal--my comment] is carried out by Howard [1970] using notations below the ordinal $\epsilon_0$. Via a formal treatment of the term model, this yields, as a by-product, an ordinal analysis: over a weak base theory [$PRA$?--my question and comment] the assertion that "there are no infinite decreasing sequences of ordinal notations beneath $\epsilon_0$" implies the consistency of $PA$.

Regarding the principle "there are no infinite descending sequences of ordinal notations beneath $\epsilon_0$", Ackermann (in his Dissertation) has this to say (this is found in Richard Zach's paper "The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program"--Zach himself says in this paper that "Ackermann was completely aware of the involvement of transfinite induction in this case [of the consistency of $2PRA^{-}$--my comment, also in the case of the proof of the consistency of $\mathbf Z_{\mathfrak a}$], but he sees in it no violation of the finitist standpoint"):

The disassembling of functionals by reduction does not occur in the sense that a finite ordinal is decreased each time an outermost function symbol is eliminated. Rather, to each functional corresponds as it were a transfinite ordinal number as its rank, and the theorem, that a constant functional is reduced to a numeral after carrying out finitely many operations, corresponds to the other [theorem], that if one descends from a transfinite ordinal number to ever smaller ordinal numbers, one has to reach zero after a finite number of steps. Now there is naturally no mention of transfinite sets or ordinal numbers in our metamathematical investigations. It is however interesting, that the mentioned theorem can be formulated so that there in nothing transfinite about it any more.

Zach continues:

Without appealing to the well-orderedness of the corresponding ordinals, it remains to argue finitistically that the finite sequences of numbers ordered in the appropriate manner are also well-ordered. Ackermann does not attempt this for the entire class of sequences of sequences of numbers needed in the proof (corresponding to $\omega^{\omega^{\omega}}$ [does the entire class of sequences of sequences of numbers needed in the proof get reduced (as it were) to a set of single numbers as resolvents in a finite number of steps?--my question and comment]), but only for $\omega^2$.

Zach now continues with Ackermann's comment:

Consider a transfinite ordinal number less than $\omega$$\cdot$$\omega$. Each such ordinal number can be written in the form: $\omega$$\cdot$$\mathfrak n$+$\mathfrak m$, where $\mathfrak n$ and $\mathfrak m$ are finite numbers. Hence such an ordinal can also be characterized by a pair of numbers ($\mathfrak n$,$\mathfrak m$), where the order of these numbers is of course significant. To the descent in the series of ordinals corresponds the following operation on the number pair ($\mathfrak n$,$\mathfrak m$). Either the first number $\mathfrak n$ remains the same, then the number $\mathfrak m$ is replaced by a smaller number $\mathfrak m^{'}$. Or the first number $\mathfrak n$ is made smaller; then I can put an arbitrary number in the second position, which can be larger than $\mathfrak m$. It is clear that one has to reach the number pair (0,0) after finitely many steps. For after at most $\mathfrak m$+1 steps I reach a number pair, where the first number is smaller than $\mathfrak n$. Let ($\mathfrak n^{'}$,$\mathfrak m^{'}$) be that pair. After at most $\mathfrak m^{'}$+1 steps I reach a number pair in which the first number is again smaller than $\mathfrak n^{'}$, etc. After finitely many steps one reaches the number pair (0,0) in this fashion, which corresponds to the ordinal number 0. In this form, the mentioned theorem contains nothing trnsfinite whatsoever; only considerations which are acceptable in metamathematics are used. The same holds true if one does not use pairs but triples, quadruples, etc. This idea is not only used in the following proof that the reduction of functionals terminates, but will also be used again and again later on, especialy in the finiteness proof at the end of the work.

It should be noted that Ackermann uses this idea in his proof of the consistency of $\mathbf Z_{\mathfrak a}$ (as is shown by Hao Wang in Chapter XIV, "ACKERMANN'S CONSISTENCY PROOF", of his book Logic, Computers, and Sets). In Chapter XIV, Wang says this about the system $\mathbf Z_{\mathfrak a}$:

The equivalence of this system with $\mathbf Z$ [Wang's notation for $PA$--my comment] holds in the sense that a theorem not containing the $\epsilon$-symbol is provable in $\mathbf Z$ if and only if it is provable in $\mathbf Z_{\mathfrak a}$.

Considering the aforementioned, I again ask the question stated in the title:

In what sense is the "descending chain principle" for ordinals less than $\epsilon_0$ 'infinitary'?

Tait (Finitism, Journal of Philosophy 78 (1981), 524-546) has argued that finitistic reasoning coincides with PRA, on the grounds that this is as far as you get with "finitist types". What makes a type "finitist" is supposed to be the idea that you can understand what an arbitrary object of that type is without having to quantify over an infinite set. If you accept this then that will explain why induction up to $\omega^\omega$ is not finitistic, since that is the proof-theoretic ordinal of PRA.
Tait's analysis is not universally accepted; for instance, see Ignjatovic (Hilbert's program and the $\omega$-rule, J. Symb. Logic. 59 (1994), 322-343).
• Ignjatovic does, however, say in the paper you mentioned that "finitistic reasoning coincides with $PRA$" is certainly acceptable as a 'working hypothesis' for the purposes of his paper. – Thomas Benjamin Feb 25 '16 at 20:40
• True, but he adds in a footnote that "one cannot rule out the possibility that any basis sufficient to justify what is formalized by PRA and which satisfies some necessary closure properties in order to be acceptable as an epistemologically distinguished system of methods, is also sufficient to justify $\varepsilon_0$-induction." – Nik Weaver Feb 25 '16 at 20:55
• Regarding $PRA$, are you aware that (at least according to Richard Zach, in the paper I referred to in my question) that Hilbert already produced a proof of the consistency of $PRA$ in his lectures of 1921-22 and 1922-23? Zach states, regarding that consistency proof, that "the idea here is the same: put a given, purported proof of 0$\ne$0 into tree form, eliminate variables, ,and reduce functionals. The remaining figure consists entirely of correct formulas, where correctness of a formula is a syntactically defined and easily decidable property. The only complication for – Thomas Benjamin Feb 26 '16 at 7:58
• (cont.) the case where function variables are also admitted is the reduction of functionals. It must be shown that every functional, i.e. every term of the language, can be reduced to a numeral on the basis of the defining recursion equations. For the original case [the consistency of $PRA$--my comment] this could be done by a relatively simple inductive proof [presumably up to $\omega^{\omega}$--my comment]." Would such a proof be defined by Ignjativic (in the paper you mention) as "almost finitistic"? And did Hilbert deem his proof 'finitistic'? – Thomas Benjamin Feb 26 '16 at 8:09