Kripke-Platek 及其他集合论中的 Kreisel-Lévy 型定理

我们证明，在带无穷公理的 Kripke-Platek 集合论（KP）之上，沿序数 ${\epsilon}_{\Omega+1}$ 的超限归纳等价于断言 KP 可靠性的模式，其中 $\Omega$ 表示论域中所有序数的上确界；这类似于如下结果：在皮亚诺算术（PA）之上，沿 ${\epsilon}_0$ 的超限归纳等价于断言 PA 可靠性的模式。在证明中，我们需要在 KP 内编码无穷证明，这是通过使用部分递归集合函数来完成的。该结果可推广到 KP + $\Gamma$-分离 + $\Gamma$-收集，其中 $\Gamma$ 为任意给定的句法复杂度，但不能推广到 ZF。