论文标题
Kreisel-lévy-type定理Kripke-Platek和其他设定理论
Kreisel-Lévy-type theorems for Kripke-Platek and other set theories
论文作者
论文摘要
我们证明，在具有无穷大（KP）的Kripke-Platek集理论上，沿序数$ε_{ω+1} $跨菲斯诱导等同于架构，其中$ω$表示$ω$的声音，其中$ω$表示宇宙中所有序言的上级;这类似于以下结果：在peano算术（PA）上，沿$ε_0$的转菲斯感应与声明PA的声音相同。在证据中，我们需要在KP中编写无限制证明，并且可以使用部分递归集合功能来完成。可以将此结果推广到KP + $γ$ - 分离 + $γ$ -Collection，其中$γ$是任何给定的句法复杂性，而不是ZF。
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.
