Notes on the Equiconsistency of ZFC Without the Power Set Axiom and Second-Order Arithmetic

We demonstrate that theories <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msup><mrow><mi mathvariant="bold">Z</mi></mrow><mo>−</mo></msup><mo>,</mo></mrow></semantics></math></inline-formula> <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msup><mrow><mi mathvariant="bold">ZF</mi></mrow><mo>−</mo></msup><mo>,</mo></mrow></semantics></math></inline-formula> <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msup><mrow><mi mathvariant="bold">ZFC</mi></mrow><mo>−</mo></msup></semantics></math></inline-formula> (minus means the absence of the Power Set axiom) and <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msub><mi mathvariant="bold">PA</mi><mn>2</mn></msub></semantics></math></inline-formula>, <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msubsup><mi mathvariant="bold">PA</mi><mn>2</mn><mo>−</mo></msubsup></semantics></math></inline-formula> (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 <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msubsup><mi mathvariant="bold">PA</mi><mn>2</mn><mo>−</mo></msubsup></semantics></math></inline-formula> via well-founded trees, as well as the Gödel constructibility in said power-less set theory.