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'?
