AI 中文总结
该研究证明Lévy-Montague反射方案Rfn在Π¹₁上对WKL₀、RCA₀保守，在Π⁰₂上对PRA保守，其结果为在对PRA保守的理论内形式化Feferman的范畴论论证开辟了道路。
AI 中文摘要
我们在二阶算术中研究Lévy-Montague反射方案Rfn：对每个公式φ，该方案断言每个集合都属于一个可数编码的ω-模型，使得φ在模型的所有参数（来自该模型）、模型与论域之间是绝对的。我们的核心结果是一个模型扩张构造：每个可数的RCA₀模型都可在不改变其一阶部分的情况下，扩张为WKL₀与完整方案Rfn的模型。由此直接可得，WKL₀+Rfn在Π¹₁上对WKL₀和RCA₀均为保守的，其一阶部分恰好是IΣ₁，且在Π⁰₂上对PRA为保守的。该结果为在对PRA保守的理论内采用Feferman利用Lévy-Montague反射完成的、基于论域的范畴论论证的ZFC形式化开辟了道路。不过，该保守性证明本身是非有限的，扩张是ω₁-塔力迫扩张的并，其不可数共尾性确保了反射。我们仅能在PRA+1-Con(Z₂)中证明该保守性，且这些结果是通过大量使用Anthropic的大语言模型Fable 5获得的。
英文摘要
We study a Lévy-Montague reflection scheme $\mathsf{Rfn}$ in second-order arithmetic: for each formula $φ$, the scheme asserts that every set belongs to a countable coded $ω$-model such that $φ$ is absolute, at all parameters from the model, between the model and the universe. Our central result is a model extension construction: every countable model of $\mathsf{RCA}_0$ can be extended, without changing its first-order part, to a model of $\mathsf{WKL}_0$ together with the full scheme $\mathsf{Rfn}$. It follows at once that $\mathsf{WKL}_0+\mathsf{Rfn}$ is $Π^1_1$-conservative over both $\mathsf{WKL}_0$ and $\mathsf{RCA}_0$, that its first-order part is exactly $\mathrm{I}Σ_1$, and that it is $Π^0_2$-conservative over $\mathsf{PRA}$. The result opens an avenue for adopting, within a theory conservative over $\mathsf{PRA}$, Feferman's $\mathsf{ZFC}$-formalization of universe-based category-theoretic arguments that was achieved using Lévy-Montague reflection. The conservation proof itself, however, is non-finitary. The extension is the union of an $ω_1$-tower of forcing extensions, and its uncountable cofinality is what secures reflection. We are only able to prove the conservation in $\mathsf{PRA}+\text{1-Con}(\mathsf{Z}_2)$. The results were obtained with extensive use of Anthropic's large language model Fable 5.
Comments26 pages
