Independence of the countable axiom of choice How does one proove that the Countable axiom of choice is not provable in ZF?Is there any brief proof?Does the Independence of the countable axiom of choice implies the independence of the axiom of choice?
 A: First of all, the easy answer.
We can prove that the axiom of choice implies the axiom of countable choice, quite easily. So by showing that the axiom of choice is consistent with the axioms of $\sf ZF$, and the negation of the axiom of countable choice is consistent as well with the rest of the axioms, we essentially prove the independence of both at once.
Of course, the axiom of choice is strictly stronger and we can use other weakened versions of the axiom of choice to prove the independence of the axiom of choice from the axiom of countable choice as well.
The harder answer is just going to be a broad strokes argument of the technical part.


*

*Godel proved that if the axioms of $\sf ZF$ are consistent, then you can define a subclass of the universe of $\sf ZF$ which satisfy $\sf ZFC$ and much much more. This class is called $L$ in modern times, and it has many many wonderful properties.
This means that if there is a model of $\sf ZF$, then there is a model of $\sf ZFC$, which alternatively means that if $\sf ZF$ is consistent then $\sf ZFC$ is consistent.

*On the other hand, Fraenkel proved that if you allowed urelements, or atoms (which are non-sets objects) to exist, then the axiom of choice is not provable. His methods were later corrected by Mostowski and improved by Specker (which is why these models are often called FM(S) models).
When Paul Cohen first described forcing, he showed how to transfer the core ideas from the existence of atoms to forcing extensions. He constructed two basic models which mimicked Fraenkel's original constructions. In both the axiom of countable choice fails pretty bad.
The basic idea is that you add to the model, using forcing, a sequence of sets which are "generic" and from the original model's point of view, they are "almost" the same. Then using one of two clever (but often equivalent) constructions, you can keep those new sets, but forget the enumeration of the sequence, in a way that leaves them un-well orderable, and in fact without a countably infinite subset.
You can find the proofs for all those, and much much more in Jech "The Axiom of Choice", as well in most modern set theory 'big books' (Jech, Kunen, Halbeisen).
A: I'm going to play fast and loose with details here, but the outline is correct. To answer your new questions: no, there is no short proof. And this only shows one direction of the indpenedence of AC, that ZF doesn't prove AC; in the other direction, we need to show that ZF doesn't disprove AC. This is proved by showing that any model of ZF contains a really nice "inner model," called "$L$," in which ZFC (and much more) is true.

OK, so the details of the proof are quite complicated, but let me give an outline:


*

*First, let's make it clear what we're going to prove. You've got your ZF axioms over here, and you want to show that they don't prove Countable Choice (CC) - assuming, of course, that ZF is consistent (otherwise it proves everything, including CC). To do this, we're going to show that if ZF is consistent, then ZF+$\neg$CC is consistent. Even thought this is a question about proofs, though, we're going to argue semantically: we'll show how, if you give me a model of ZF, I can give you a model of ZF+$\neg$CC. By Completeness + Soundness, this means that if ZF is consistent then ZF+$\neg$CC is consistent.

*So this is going to be a relative construction: we'll start with some $V$ in which the ZF axioms (in fact, the ZFC axioms) are true, and we'll build a $W$ in which the ZF axioms are still true, and CC is false. In order to do this, though, we need some method to build models of ZF which gives us some measure of control over their properties. And this is really hard, since it's not even clear how to build models of ZF at all!

*The trick is forcing. Given a partial order $\mathbb{P}$, we can think of the elements of $\mathbb{P}$ - conditions - as approximations to some bigger object. For example, if $\mathbb{P}$ is the set of finite binary strings, then an element of $\mathbb{P}$ is an approximation of a real number - an infinite binary string. Think of a condition as providing incomplete information about something we're trying to build; specifically, the thing the condition is approximating is a maximal filter through $\mathbb{P}$. This isn't by itself a new idea - this is how the Baire category theorem goes, and Cantor's diagonal proof.

*OK, so what do posets have to do with models of ZF? To answer that question, let's talk about something completely different - the idea of an conditional name for a set. Remember that a model of ZF is built in layers - we start with $\emptyset$ as our 0th layer, and take powersets and limits to get successive layers, continuing all the way up the ordinals. (This can actually be formalized and proved as a theorem of ZF - the crucial axiom is Foundation.) This means we can think of a set as a well-founded tree, or as an instruction for how to build a set which is appropriately non-circular, e.g. the instructions


*

*"This set has $\omega$-many elements;"

*"The first element has one element;"

*"That element has no elements;"

*"The second element has one element;"

*"That element has one element;"

*"That element has no elements;"

*. . .



describe the set $\{\{\}, \{\{\}\}, \{\{\{\}\}\}, . . .\}.$


*

*Now, we could imagine a similar set of instructions which were conditional - e.g., "This set is the emptyset if my name is Steve, and otherwise is the set containing the emptyset." These things feel like sets in a lot of ways, but they aren't quite - in the same way that a formula isn't a sentence without evaluating the free variables, or a polynomial isn't a set of points without describing the field its over, these names aren't really referring to individual sets. Still, they're not far off: we can evaluate names, once we supply sufficient information - for example, once I tell you my name isn't Steve you know the name above refers to the set $\{\{\}\}$.

*So here's an idea for how to, given a model $V$ of ZF, build a new "thing" $W$: take all the names in $V$ which refer to only a certain kind of information - say, "names of people" - provide some "complete information" - say, everyone's name - and then evaluate all those names to produce actual sets; and say $W$ is the collection of all the sets produced in that way.

*Oh hey, I used the word "complete" - that sounds like what I said about posets! In fact, for our purposes, a "name" will be "an ambiguous description of a set, which depends on questions of the form "Is $x$ in $G$?" where $G$ is only known to be a maximal filter of some fixed poset $\mathbb{P}$." Formally, the class of $\mathbb{P}$-names is defined inductively, as: $$\mbox{A $\mathbb{P}$-name is a set of ordered pairs $(p, \nu)$, where $p\in\mathbb{P}$ and $\nu$ is a $\mathbb{P}$-name;}$$
$$\mbox{the *evaluation* $\mu[G]$ of a name $\mu$ on a max. filter $G\subseteq\mathbb{P}$ is $\mu[G]=\{\nu[G]: \exists p\in G((p, \nu)\in \mu)\}$.}$$
That is, thinking of $\mu$ as a set of instructions for how to build a set, we're looking at instructions of the form "If $p\in G$, then put (the thing defined by the following sub-instructions) into our set; otherwise, ignore (the following sub-instructions)."

*Now here's the neat bit: it turns out that if $V$ is a countable (not a problem, use Lowenheim-Skolem) model of ZFC, $\mathbb{P}\in V$ is a poset, and $G$ is a maximal filter through $\mathbb{P}$ which meets every dense subset of $\mathbb{P}$ living in $V$ - called a generic filter; note that this means $G\not\in V$, probably - then $V[G]$, the set of all $\mathbb{P}$-names in $V$ evaluated at $G$, is a model of ZFC! (We call such a $V[G]$ a generic extension of $V$.) So this is great . . .

*. . . except we don't want choice to hold. And this is a problem - if we assume merely "ZF is consistent," the only model we can easily describe is $L$, which satisfies ZFC. So we need some way to start with a model of ZFC, and turn it into a model where choice fails.

*To do this, we go back to the description of $V[G]$, and make it smaller - rather than throw in all the names, well restrict attention to good names for some value of "good." It turns out that the right notion of "good" here has to do with families of groups of automorphisms of $\mathbb{P}$ - roughly, a name is good if it is fixed by one of the groups of automorphisms. Different families of automorphisms give rise to different notions of good - and in particular, if our family includes the trivial group, then every name is good. It turns out that we preserve the axioms of ZF by doing this, so this is a viable construction to try.

OKAY, THAT WAS LONG. So let me very briefly describe how the actual construction goes: 


*

*Start with $V\models ZFC$ countable.

*Let $\mathbb{P}$ be the poset $((2^{<\omega})^\omega)^\omega$ - basically, an element of $\mathbb{P}$ is an approximation to a countable family of countable families of reals - or, we're building countably many "blocks" of countably many rows, and each row represents a real. 

*For $F$ a finite set of rows, let $S_F$ be the set of automorphisms of $\mathbb{P}$ which only act by swapping rows, don't swap rows between blocks, and don't move the rows in $F$. 

*Then the resulting "good names" give the model we're looking for - our generic filter $G$ is (basically) a countable collection of sets of reals, but no choice function has a good name. 
