I'm trying understand how that the Well-Ordering Theorem holds in the theory ZC. I know that Zermelo gave a proof in 1904, of which I found a very rough sketch. But I don't see how it would works.
The sketch starts like this, which is just definitions:
Let $s$ be a set. By $\mathsf{AC}$, we know that there is a choice function $f$ on $\mathcal{P}(s)-\emptyset$. For each $x\in \mathcal{P}(s)-\emptyset$, say that $x$ is an $f$-set if there exists some well-order $R_x\subset x\times x$ such that for any $m\in x$ we have $f(\{e\in s: e\notin x \vee (e, m)\notin R_x\})= m$.
Now, the real proof begins:
The sketch says to observe that there are nonempty $f$-sets, giving the example $D$ where $b: = f(s)$ and $D=\{b\}$. But I don't see how this satisfies the criteria of an $f$-set.
Next, it says that we can show that if $Y$ is an $f$-set with well-order $\leq_Y$ and $Z$ is an $f$-set with well-order $\leq_Z$, then $Y \subset Z$ and $\leq_Z$ is an extension of $\leq_Y$ or vice-versa. One then takes the union of the $f$-sets and shows that this union is an $f$-set which exhausts $s$.
I have no intuition for how this would actually work.
Does anyone know where I could find a full proof along these lines? Alternatively, does anyone know the proof and is willing to reproduce it? I'd appreciate any feedback.
Why is $D$ an $f$-set? As $D$ is a singleton, the exists a well-order $R_D$, namely $R_D=\emptyset$ (because $b\not<b$). Then for the only $m=b\in D$ that needs to be tested, we have $\{\,e\in s:e\notin D\lor (e,b)\notin \emptyset\,\}=\{\,e\in s:e\notin D\lor \top\,\}=s$ and so $f(s)=m$, as desired.
The intuition you should have is that the sets of the form $\{\,e\in s:e\notin x\lor (x,m)\notin R_x\,\}$ are the complements of initial segments of the well-ordered set $x$. And for an $f$-set, $f$ maps such (a complement of) an initial segment to the next-biggest element of $x$.
Next, let $Y,Z$ be $f$-sets with respective well-orders. Let us assume that $Z\not\subseteq Y$.We want to show (among others) that $Y\subseteq Z$. For $y\in Y$ let $I^Y_y:=\{\,x\in Y:x<_Y y\,\}$ and for $z\in Z$ let $I^Z_y:=\{\,x\in Z:x<_Z z\,\}$. Note that $f(s\setminus I^Y_y)=y$ for all $y\in Y$ and $f(s\setminus I^Y_z)=z$ for all $z\in Z$. Define $$\phi(t)\equiv t\in Y\cap Z\land I^Y_t=I^Z_t\land {(<_Y)}\cap {I_t^Y\times I_t^Y}={(<_Z)}\cap {I_t^Z\times I_t^Z}. $$ Let $y\in Y$ and suppose that $\phi(t)$ holds for all $t\in Y$ with $t<_Yy$. As $Z\not\subseteq Y$, let $z$ be the $<_Z$-minimal element $z$ of $Z\setminus I^Y_y$. Then $I^Z_z=I^Y_y$. But that means $z=f(s\setminus I^Z_z)=f(s\setminus I^Y_y)=y$. Therefore $y\in Z$ and the remaining parts of $\phi(y)$ follow readily. By transfinite induction (over $Y$ with its well-order $<_Y$) we conclude that $\phi(t)$ holds for all $t\in Y$. In particular, $Y\subseteq Z$, but also $(<_Y)=(<_Z)\cap Y\times Y$.