Timeline for A proof of $ZF \vdash AC^L$

6 events

when toggle format	what		by	license	comment
Jul 10, 2012 at 12:00	vote	accept	Archbishop
Jul 9, 2012 at 17:28	comment	added	Archbishop		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).
Jul 9, 2012 at 17:11	comment	added	Andreas Blass		@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.
Jul 9, 2012 at 17:06	history	edited	Andreas Blass	CC BY-SA 3.0	fixed a serious typo
Jul 9, 2012 at 17:01	comment	added	Archbishop		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$.
Jul 9, 2012 at 16:50	history	answered	Andreas Blass	CC BY-SA 3.0