FOM: re. mathematical induction

[Charles Parsons]

>
>I don't know Ryll-Nardzewski's proof. But the following argument for
>non-finite axiomatizability of PA would have been available from the
>1930's---in the sense of being immediate from what was known: By Gentzen's
>proof of his Hauptsatz, and this is provable in PRA, every proof in PA of a
>formula of (logical) complexity < n using induction only on formulas of
>complexity < n can be assumed to involve only formulas of complexity < n.
>(Eliminate all cuts with cut formula of complexity >= n.) But the
>consistency of PA with cuts and induction so restricted is provable in
>PRA+induction up to omega(n+1) [where omega(0)=omega and omega(k+1)=omega
>exp omega]. This is immediate from Gentzen's consistency proof for PA.
>
>Bill

Bill Tait is no doubt right that the argument he cites "would have been
available from the 1930's". That is to say, someone looking at Gentzen's
work and working out how the ordinals involved depended on the complexity
of the formulae in the proof should have been able to figure it out. But I
don't know of anyone's having done that until after Ryll-Nardzewski's proof
became known. (I did it (for Schuette's proof) in my dissertation, but by
sheer stupiidity didn't get the most refined ordinal bounds, which I only
got in 1966. No one else had published on the subject up to then, although
Mints did a little later.)

I'm embarrassed to say that it's only now that I've learned that Mostowski
gave in the 1952 paper an argument for the non-finite-axiomatizability of
PA that I learned from a somewhat later paper by Kreisel and Wang: "Some
applications of formalized consistency proofs", FM 42 (1955), 101-110.
Ryll-Nardzewski's proof was model-theoretic, using Skolem's non-standard
model construction.

Charles Parsons