A constructive consistency proof of a fragment of set theory
type: Item
instance of: scholarly article
title: A constructive consistency proof of a fragment of set theory
zbMATH Open document ID: 0599.03059
DOI: 10.1016/0168-0072(84)90034-4
author: Jon Pearce
published in: Annals of Pure and Applied Logic
publication date: 1984-01-01T00:00:00Z
review text: 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.
reviewed by: F.R.Drake
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03E35
zbMATH DE Number: 3966069
zbMATH Keywords: Kripke-Platek set theory
zbMATH Keywords: inaccessibility scheme
zbMATH Keywords: second-order arithmetic
zbMATH Keywords: bound
zbMATH Keywords: primitive recursive well-ordering
zbMATH Keywords: cut-elimination
zbMATH Keywords: fragement of infinitary logic
zbMATH Keywords: ordinal notations
MaRDI profile type: Publication
full work available at URL: 0168-0072(84)90034-4
OpenAlex ID: W2016940265
cites work: Q4075450
cites work: A simplification of the Bachmann method for generating large countable ordinals
cites work: Q4109654
cites work: Q3895467
cites work: Q5533181
cites work: Q3874169
cites work: The varieties of arboreal experience
cites work: Q5519134
cites work: Q5605873
cites work: Q5638276
description: scientific article; zbMATH DE number 3966069