Kreisel-L\'evy-type theorems for Kripke-Platek and other set theories

MaRDI QIDQ6419680zbMATH OpenFDO

Authors Shuangshuang Shu, Michael Rathjen

Publication date 6 December 2022

Abstract: We prove that, over Kripke-Platek set theory with infinity (KP), transfinite induction along the ordinal ${epsilon}_{Omega+1}$ is equivalent to the schema asserting the soundness of KP, where $Omega$ denotes the supremum of all ordinals in the universe; this is analogous to the result that, over Peano arithmetic (PA), transfinite induction along ${epsilon}_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 + $Gamma$-separation + $Gamma$-collection where $Gamma$ is any given syntactic complexity, but not to ZF.

This page was built for publication: Kreisel-L\'evy-type theorems for Kripke-Platek and other set theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6419680)