FOM: re. mathematical induction

[William Tait]

Mic Detlefsen (2/1) wrote
>(Local Reflexivity for ZFC): For every finitely axiomatizable subsystem
>F-zfc of ZFC, Con(F-zfc) is provable in ZFC.
>
>[Note: Mostowski proved this in 1952 in a paper entitled 'On Models of
>Axiomatic Systems', FM 39: 133-158. In the same paper, he also proved the
>'reflexivity' of PA and a certain first-order system of real arithmetic R.
>At the time this was proved, I believe that it was the only means available
>for proving the non-finite axiomatizability of PA. Later the same year, and
>in the very same volume of FM, however, Ryll-Nardewski published a paper
>('The Role of the Axiom of Induction in Elementary Arithmetic', FM 39:
>239-263) giving a more 'direct' proof of the non-finite axiomatizability of
>PA.]

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