A constructive consistency proof of a fragment of set theory (Q1080422)

The fragment of set theory, S, is Kripke-Platek set theory plus the inaccessibility scheme. This has a new function symbol \(+\), the axiom \(\forall x [ord(x^+)\&(ord(x)\to x\in x^+)]\) and the relativized collection scheme \(\forall x coll(\phi)^{L(x^+)}\) (where \(\phi\) has no unbounded quantifiers and coll(\(\phi)\) is \(\forall u\in v \exists y \phi (u,y)\Rightarrow \exists z \forall u\in v \exists y\in z \phi (u,y)).\) \textit{W. Tait} [Intuitionism and proof theory, Proc. Summer Conf. Buffalo N.Y. 1968, 475-488 (1970; Zbl 0231.02033)] gave a consistency proof for second-order arithmetic \(\Sigma^ 1_ 2-AC+BI\), and this can be interpreted in S. The present proof improves Tait's work by giving an exact bound on the primitive recursive well-ordering needed for the proof of cut-elimination. As usual this gives a bound on the provably well- founded recursive orderings of the theory [see: \textit{S. Feferman}, Handbook of mathematical logic, 913-971 (1978; Zbl 0443.03001)]. The proof proceeds by translating S into a fragement of infinitary logic and applying a cut-elimination argument adapted from Tait; the ordinal notations required are set out in detail.