Lévy–Montague reflection is $\Pi^1_1$-conservative over $\mathsf{WKL}_0$

We study a Lévy–Montague reflection scheme $\mathsf{Rfn}$ in second-order arithmetic: for each formula $\phi$, the scheme asserts that every set belongs to a countable coded $\omega$-model such that $\phi$ 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 $\Pi^1_1$-conservative over both $\mathsf{WKL}_0$ and $\mathsf{RCA}_0$, that its first-order part is exactly $I \Sigma_1$, and that it is $\Pi^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 $\omega_1$-tower of forcing extensions, and its uncountable cofinality is what secures reflection. We are only able to prove the conservation in $\mathsf{PRA} + {1 \text{-} \mathsf{Con}} \left( \mathsf{Z}_2 \right)$ where ${1 \text{-} \mathsf{Con}}$ stands for `$1$-consistency', i.e. uniform $\Pi^0_2$-reflection. The results were obtained with extensive use of Anthropic's large language model ‘Fable 5’.