Consistency proof via pointwise induction (Q1128178)

To show the consistency of PA, Gentzen assigned an ordinal number \(o({\mathcal P})<\varepsilon_0\) to a purported proof of contradiction and also defined a reduction \(r({\mathcal P})\). He showed that \(o(r({\mathcal P}))< o({\mathcal P})\), and thus that transfinite induction up to \(\varepsilon_0\) proves the consistency of PA. By modifying (formal) proofs and ordinal assignments, the author improves this approach in two ways: (1) he shows that \(o(r({\mathcal P}))= o({\mathcal P})[1]\), where for an ordinal \(\alpha\), \(\alpha[n]_{n\in\omega}\) is the fundamental sequence to \(\alpha\), and (2) he considers not only PA but also systems \(\text{ID}_q\), \(q\in\omega\), of finitely iterated inductive definitions. The price he pays is that he uses the Howard ordinal (which is much larger than \(\varepsilon_0\)). Actually, he shows the consistency of these systems in elementary recursive arithmetic with pointwise induction (i.e. transfinite induction whose assumption at a limit ordinal \(\lambda\) involves a constant point of its fundamental sequence and is thus independent of \(\lambda\) itself -- in this case \(\lambda[1]\)).