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

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.