Consistency Proof via Pointwise Induction
Andreas Weiermann, Toshiyasu Arai · Bulletin of Symbolic Logic · 2002
We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal.Our proof differs from U. Schmerl [S]: We do not need Girard's Hierarchy Comparison Theorem.A modification on ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha[1]$ in ordinals.Also a generalization to theories $ID_{q}$ of finitely iterated inductive definitions is proved.We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal.Our proof differs from U. Schmerl [S]: We do not need Girard's Hierarchy Comparison Theorem.Let $P$ be a proof of the empty sequent in $PA$ or the second order arithmetic $\Pi_{1}^{1}-CA0$ .For such a proof $P$ let $o(P)$ denote the ordinal assigned to $P$ and $r(P)$ a reduct of $P$ defined by Gentzen and Takeuti [T].$r(P)$ is again a proof of the empty sequent and $o(r(P)) 0)\Rightarrow(a_{0}, \ldots , a_{k})\in T(q)$ 2. For $a_{0},$ $\ldots,$ $a_{k}\in PT(q)$ and $k\in \mathrm{t}^{-1,0}$ }, we set $(a_{0}, \ldots, a_{k})=\{$