把Lévy-Montague反射做到WKL₀上的论文，给了保守性证明，还用了Fable 5辅助推证。
论文研究二阶算术中的Lévy-Montague反射方案Rfn：每个公式φ都断言任意集合属于某个可数编码的ω-模型，且φ在该模型与宇宙间绝对。核心结果是模型扩张构造：每个RCA₀的可数模型都可在不改变一阶部分的情况下扩张为WKL₀加上完整Rfn的模型。由此推出WKL₀+Rfn对WKL₀和RCA₀都是Π¹₁-保守的，其一阶部分恰为IΣ₁，且对PRA是Π⁰₂-保守的。证明本身非有限性：扩张是ω₁-层强迫扩张的并，其不可数共尾性保证了反射；作者仅在PRA+1-Con(Z₂)中证明了该保守性。
Lévy-Montague reflection is $Π^1_1$-conservative over $\mathsf{WKL}_0$
We study a Lévy-Montague reflection scheme $\mathsf{Rfn}$ in second-order arithmetic: for each formula $\varphi$, the scheme asserts that every set belongs to a countable coded $ω$-model such that $\varphi$ 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.