# Is there a proof of independence of AC from Z that is done in Z?

The proof that $$AC$$ is independent of $$\sf ZF$$ axioms is done by forcing and constructibility, and these don't beg any consistency strength more than that of $$\sf ZF$$.

Is there a known similar proof of independence of $$AC$$ from $$\sf Z$$ that is done at the consistency level of $$\sf Z$$ itself?

More generally what is the smallest consistency level we need to prove that $$AC$$ is independent from axioms of $$\sf Z$$?

• To clarify, you're asking whether $\mathsf{Z}$ (or even less) can prove "If $\mathsf{Z}$ is consistent then so are $\mathsf{ZC}$ and $\mathsf{Z+\neg AC}$"? I think Mathias has some relevant results but the papers are quite long and my memory is vague. Sep 22 at 18:30
• @NoahSchweber, Yes! In particular the same question in connection to MacLane set theory is of interest. Sep 22 at 18:42

I have not read it myself yet, but it seems that the relative consistency of $$\mathsf{AC}$$ with $$\mathsf{Z}$$ was proved by Mathias in his paper The strength of MacLane set theory. To quote Mathias' summary (available here):
Of course this leaves open the question of whether $$\neg\mathsf{AC}$$ is also relatively consistent with $$\mathsf{Z}$$. In the absence of replacement, forcing becomes quite tricky, so the "usual" approach seems fraught to say the least. Mathias has intensely studied forcing over weak set theories (leading up to his analysis of and advocacy of "provident set theory" $$\mathsf{Provi}$$ in this context), but at a quick glance I don't see any results that suffice here. I suspect, though, that the answer is again affirmative.
• @ZuhairAl-Johar Even making sense of $\nu[G]$ for a name $\nu$ needs replacement I think. Sep 23 at 14:55