Consistency of Choice

If Zermelo-Fraenkel Set Theory is consistent, then Axiom of Choice is consistent:

Proof

Suppose is consistent. By Gödel’s Completeness Theorem for First-Order Logic take

(in the meta-theory). Let be the Constructible Hierarchy in . As is the Constructible Model of Set Theory we have

We can provide a Well-Order of : Let be what thinks that is. Note that is Absolute between and , but might not be the same as in . Fix some some on of Order Type Assume that is a Well-Order of , and let be the set of formulas encoded in . Define lexicographically a Well-Order of

and then write for

Make this into an end-extension of by

Thus

is a well-order of (as seen by ) This was a recursive definition so it is Absolute. As is a Transitive Model in :

and thus

As is a set in the meta-theory, we proved: