Consistency proof via pointwise induction
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]\)).
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- The \(\omega\)-consistency of elementary analysis
- Iterated local reflection versus iterated consistency
- Inductive definitions over a predicative arithmetic
- Where is the Gödel-point hiding: Gentzen’s Consistency Proof of 1936 and His Representation of Constructive Ordinals
- Variations on a theme by Weiermann
- How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
- Intuitionistic fixed point theories over set theories
- Reduction of higher type levels by means of an ordinal analysis of finite terms
This page was built for publication: Consistency proof via pointwise induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1128178)
