Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA
Vladimir Kanovei, Vassily Lyubetsky
TL;DR
Addresses the equiconsistency of $PA_2^{-}$, $PA_2$, and weak set theories $Z^{-}$, $ZF^{-}$, $ZFC^{-}$ when Power Set is omitted. The authors develop a power-less framework $ ext{TMC}$ and realize interpretations of $ ext{TMC}$ inside $PA_2^{-}$ via well-founded trees, then embed a Gödel-constructibility-style hierarchy $L^{*}$ within $ ext{TMC}$ to interpret $ZFC^{-}$, yielding mutual interpretability and equiconsistency. Key contributions include a concrete two-direction interpretability, the construction of ${{f L}^{ullet}}$ and related models modeling $ZFC^{-}$, and the result that ${f L} estriction oldsymbol{ ext P}(oldsymbol{ ext ω})$ models $PA_2$ within $PA_2^{-}$. The work also outlines alternative models (e.g., ${f L}^{ extdagger}$, ${f L}^{ extddagger}$, HCL) and sketches a ramified analytical pathway to a purely analytical equiconsistency proof, highlighting implications for forcing and foundational analyses. Overall, the paper provides a self-contained bridge between second-order arithmetic and weak set theories, yielding new models and guiding future analytical and forcing-based investigations.
Abstract
We demonstrate that theories $\text{Z}^-$, $\text{ZF}^-$, $\text{ZFC}^-$ (minus means the absence of the Power Set axiom) and $\text{PA}_2$, $\text{PA}_2^-$ (minus means the absence of the Countable Choice schema) are equiconsistent to each other. The methods used include the interpretation of a power-less set theory in $\text{PA}_2^-$ via well-founded trees, as well as the Gödel constructibility in the said power-less set theory.