Well-ordering theorem and second-order logic
I am confused by this sentence in the Wikipedia article for "Well-ordering theorem":
...the well-ordering theorem is equivalent to the axiom of choice, in the sense that either one together with the Zermelo–Fraenkel axioms is sufficient to prove the other, in first order logic (The same applies to Zorn's Lemma.) . In second order logic, however, the well-ordering theorem is strictly stronger than the axiom of choice: from the well-ordering theorem one may deduce the axiom of choice, but from the axiom of choice one cannot deduce the well-ordering theorem
Isn't second-order logic stronger than first-order logic? How is it that the equivalence proof in first-order logic is no longer valid in second-order logic?
Solution 1:
If you follow the references given in the Wikipedia article, you will find out that the context of this theorem is very different.
While a lot of mathematics is done inside models of $\sf ZFC$ with first-order logic (and so we can make statements about high order logic inside the model). However one can use second-order logic (or rather some systems of second-order logic) as a foundation for mathematics. That is, we no longer work in $\sf ZFC$, we work in a context of second-order logic.
In certain systems which include the axiom of choice, the well-ordering principle is not provable. However without using the axiom of choice it is not hard to show that the well-ordering principle still implies the axiom of choice.
This is essentially theorem 5.4 which you can find on page 107 in the book by Shapiro.
Solution 2:
There is a separate issue with trying to interpret this claim from the Wikipedia article:
In second order logic, however, the well-ordering theorem is strictly stronger than the axiom of choice: from the well-ordering theorem one may deduce the axiom of choice, but from the axiom of choice one cannot deduce the well-ordering theorem
In second-order arithmetic, the "well ordering theorem" is trivial: it is usually taken to mean that every set of natural numbers has a least element, which is a trival consequence of an induction axiom. It is hard to even state in second-order arithmetic that "there is a well ordering of the class $S$ of all subsets of $\mathbb{N}$" because, syntactically, that is a third-order statement. One could assert that there is a definable well-ordering of $S$ by referring to a particular formula that defines the well-ordering, but there is no reason to suspect that there is, in fact, a definable well ordering of $S$ unless we also assume something like $V = L$.
However, in second-order arithmetic, the "axiom of choice" is typically phrased as an axiom scheme. And, it is usually studied in a form where the objects being chosen are sets, not natural numbers. A typical instance of the scheme says: $$ (\forall n)(\exists Y)\Phi(n,Y) \to (\exists Z)(\forall m)\Phi(m,(Z)_m) $$ where $(Z)_m = \{ k : \langle m,k\rangle \in Z\}$. See Simpson, Subsystems of Second-order Arithmetic, section VII.6.
Now the well-ordering theorem for numbers does not imply the scheme for the axiom of choice for sets that I just described. Indeed, the full axiom system for second-order arithmetic, with comprehension for all formulas, does not even prove all instances of the axiom of choice in which $\Phi$ is $\Sigma^1_3$ (Simpson VII.6.3).
The key issue here is that, while "axiom of choice" makes fine sense in terms of type theory, such as second-order arithmetic and second-order logic more generally, it does not mean at all the same thing that it does in the "untyped" language usually used for set theory.