I've recently read that ZF is equi-consistent to ZFC. From what I understand, to establish this we transform a formal proof of a contradiction in ZFC into a formal proof of a contradiction in ZF.
We do this by constraining all quantifications to the constructible universe : $\forall x,\phi$ is replaced by $\forall x, \text{Constructible}(x)\Rightarrow \phi$ and $\exists x,\phi$ is replaced by $\exists x, \text{Constructible}(x)\land\phi$. Because the constructible universe is an inner model, this syntactic transformation produces a valid formal proof, that respects inference rules.
And the invocations of the axiom of choice become
$$\forall x, \text{Constructible}(x)\Rightarrow \exists f, \text{Constructible}(f)\land \text{ChoiceFunction}(f,x)$$
But that is no longer an axiom, it is a theorem of ZF. Therefore we have a formal proof of a contradiction in ZF. Is this correct?
I am wondering how far we can continue these equi-consistency proofs in ZF. Can we remove the axiom of foundation ? Even the axiom of infinity ? I doubt it because, if we could remove all axioms, ZFC would be equi-consistent with the empty theory, which is consistent.
Best Answer
Yes, you can remove the axiom of foundations by the same argument: move from a universe of $\sf ZF-Fnd$ to the von Neumann universe, which is the largest well-founded and transitive class.
When you remove Infinity, Power set, or Replacement, you get strictly weaker theories. To see why, note that $V_\omega,\mathrm{HC}$ and $V_{\omega+\omega}$ are models of $\sf ZF-Infinity, ZF-Power, ZF-Replacement$ respectively. Therefore $\sf ZF$ proves these theories have a model, so they are consistent. In particular by Gödel's theorem none of them can prove that $\sf ZF$ itself is consistent.