Cut-elimination for ω₁

2018/01/27 by Arai, Toshiyasu
#03F99 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1801.10025

Abstract

In this paper we calibrate the strength of the soundness of a Kripke-Platek set theory with the axioms of Infinity and Π₁-Collection with the assumption that`there exists an uncountable regular ordinal' in terms of the existence of ordinals.

Related

• omega₁ under Pi₁-Collection
• Kreisel-Lévy-type theorems for Kripke-Platek and other set theories
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• Classifying the provably total set functions of KP and KP(P)
• An ordinal analysis of Π₁-Collection