Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA

TL;DR

This paper shows that certain set theories without the Power Set axiom are equiconsistent with second order PA, using interpretations via well-founded trees and G"odel constructibility.

Contribution

It establishes the equiconsistency of ZF-, ZFC-, and second order PA theories without the Power Set axiom and Countable Choice schema.

Findings

Equiconsistency of ZF-, ZFC-, and second order PA without Power Set.

Use of well-founded trees to interpret power-less set theories.

Application of G"odel constructibility in power-less set theories.

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\"odel constructibility in the said power-less set theory.