# 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

Towards a partial answer:

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):

The paper shows that Z + AC is indeed consistent relative to Zermelo's system Z, but the inadequacy, demonstrated in Slim Models, of Z for recursive constructions necessitates an oblique approach.

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.

• I'm curious! Where do exactly Replacement is needed in forcing, I mean the names\values construction do not really needs the full power of Replacement, a theory like Z+ranks would be enough to do it, is it in the proofs about the forcing language which ensures the generic extension to be a model of the background theory?? Where exactly? Sep 23 at 14:10
• @ZuhairAl-Johar Even making sense of $\nu[G]$ for a name $\nu$ needs replacement I think. Sep 23 at 14:55
• hmmm.. I thought this can be done in Z+ ranks. Sep 23 at 15:23
• @ZuhairAl-Johar I could be wrong, but I don't believe that's the case (I haven't thought about it very hard though). Sep 23 at 16:33
• I think the relevant article is: Provident sets and rudimentary set forcing, by Mathias. Can be found at Researchgate: researchgate.net/publication/…. The answer to this question is affirmative! You pass to the provident closure of a model of Z, and work inside that model (Mathias). Sep 30 at 9:33