vix.ing · top · new · best · stats · spec

Kreisel-Lévy-type theorems for Kripke-Platek and other set theories

2022/12/06 by Shuangshuang Shu, Shu, Shuangshuang, Michael Rathjen +1
Mathematics · #Advanced Topology and Set Theory #FOS: Mathematics #Functional Equations Stability Results #Logic (math.LO) #Mathematical Dynamics and Fractals

paper · pdf · doi:10.48550/arxiv.2212.02843

openalex publication_date 2022/12/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We prove that, over Kripke-Platek set theory with infinity (KP), transfinite induction along the ordinal εΩ+1 is equivalent to the schema asserting the soundness of KP, where Ω denotes the supremum of all ordinals in the universe; this is analogous to the result that, over Peano arithmetic (PA), transfinite induction along ε0 is equivalent to the schema asserting the soundness of PA. In the proof we need to code infinitary proofs within KP, and it is done by using partial recursive set functions. This result can be generalised to KP + Γ-separation + Γ-collection where Γ is any given syntactic complexity, but not to ZF.

Related