A new model construction by making a detour via intuitionistic theories III: Ultrafinitistic proofs of conservations of Σ11 collection

摘要

© 2022Along the line of the making-a-detour method that the author (partially with Zumbrunnen) has invented and developed in the previous works of his, in this article we obtain several conservation results on the second order collection schema (∀X∈U)∃Yφ[X,Y]→∃V(∀X∈U)(∃Y∈V)φ[X,Y] and the second order closure schema ∀x,Y∃Zφ[x,Y,Z]→∃V∀x(∀Y∈V)(∃Z∈V)φ[x,Y,Z] in second order arithmetic. Particularly, (Σ11-Coll) and even (Σ11-Clos) are Π21 conservative over WKL0 and WKL0⁎ (and hence Π11 conservative over RCA0 and RCA0⁎). Moreover, (Σ11-Coll) is Π21 conservative over Δ11-CA0 and so is (Σ11-Clos) over Δ11-CA0+(Πn+11-Ind) where (Σ11-Coll) and (Σ11-Clos) are equivalent over ACA0 to (Σ11-AC) and (Σ11-DC) respectively. Unlike usual model- and proof-theoretic proofs, all the proofs are by giving concrete interpretations and hence effective in the sense of polynomial-time. Thus the reductions are, in this sense, ultrafinitistic and free from speed-up of exponential or more. The reader's familiarity to the previous papers in this series would help but is not required.