MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I'm studying Set Theory on my own and I have a question about a proof. The book I am reading wants to prove $ZF \vdash (AC)^L$ in order to prove the relative consistency of AC from ZF. I have no problems with the proof of the following theorem:

1) $ZF \vdash (V = L)^L.$

Here comes the problem: my book is a bit concise and I am not sure if the following proof of mine is correct. It would be very kind if you could check it:

We have a formula $\Phi$ which is $\exists \xi \psi$ where $\psi$ is $\Delta^{ZF}_1$ (I do not know if you are familiar with this $\psi$ but it should be the canonical well-ordering of $L$), so from 1 we have $$ZF \vdash \forall x \in L (\Phi \text{ Well orders } x)^L$$ which is equivalent to $$ZF \vdash \forall x \in L (\Phi^L \text{ Well orders } x)$$ (because the formula $\Phi^L \text{ Well orders } x$ is $\Delta_1^{ZF}$)

which is equivalent to $$ZF \vdash \forall x \in L (\Phi \text{ Well orders } x)$$ (because $\Phi$ is $\exists \xi \psi$ and all the ordinals are in $L$)

which is $$ZF \vdash WOT^L$$ (where WOT is the Well Ordering Theorem)

But also $ZF \vdash WOT \leftrightarrow AC$ so $ZF \vdash AC^L$.


Note: The last passage works because we have $ZF \vdash WOT^L \leftrightarrow AC^L$ because $WOT \leftrightarrow AC$ is $\Delta_1^{ZF}$.

share|cite|improve this question
up vote 5 down vote accepted

If you write out in the obvious way the equivalence $WOT\iff AC$, it won't be $\Delta_1$; the ony reason it's $\Delta_1^{ZF}$ is that it's provable in ZF (hence provably equivalent to $0=0$).

My general impression of your argument is that you're making things unnecessarily complicated. Once you have that ZF proves the relativizations to $L$ of the axioms of ZF and of $V=L$, then it follows by general logic (not anything specific to set theory) that "ZF + ($V=L$)" is consistent if ZF is. Since AC is provable in the theory "ZF + ($V=L$)", it follows (still by general logic) that "ZF + AC" is consistent if ZF is.

share|cite|improve this answer
I suppose you mean 0 = 0, a tautology. I know I am making things a bit too complicated but for reasons which would take too long to explain I need an explicit proof of $ZF \vdash AC^L$. – Archbishop Jul 9 '12 at 17:01
@Archbishop: Thanks for the correction; I've edited it into the answer. For an explicit proof of $AC^L$ in ZF, take the proof of AC from ZF plus $V=L$; relativize everything to $L$; and, wherever the original proof used $V=L$ or a ZF-axiom $\alpha$, insert the proof from ZF of $(V=L)^L$ or of $\alpha^L$. Depending on how you formalized logic, you may also need to insert justifications for the relativizations of logical axioms and rules. This is what I had in mind with "general logc" in my answer. – Andreas Blass Jul 9 '12 at 17:11
Thank you very much for the tautology thing. I totally missed it. Now even the Drake's proof makes sense. He proves that $ZF \vdash (V=L)^L$ and $ZF \vdash V=L \rightarrow AC$. Then he claims $ZF \vdash AC^L$ and that is because $V=L \rightarrow AC$ is equivalent to $0 = 0$, so we also have $ZF \vdash (V=L)^L\rightarrow AC^L$ (and L is a model of ZF). – Archbishop Jul 9 '12 at 17:28

The usual strategy is to define inductively a well-ordering on $L(\alpha)$ for each ordinal $\alpha$. Since under the assumption $V=L$, any set $x \in L (or$ $V), x\subseteq L(\beta)$ for some $\beta \in ORD$, thus $x$ is well-orderable. I guess your approach is correct. I suppose the canonical well-ordering you are talking about is as that in Kunen's book.

share|cite|improve this answer
It is from Drake's book, but it should be more or less the same, if I remember correctly. – Archbishop Jul 9 '12 at 17:03

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.