# 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?

-
By "second-order logic" they don't mean ZF+"second-order logic", they mean pure second-order logic", which is a kind of impoverished set theory. You have "individuals" (aka "atoms" or "urelements") and sets of individuals, but no sets of sets, those come with third order logic. – bof Oct 12 '13 at 6:23

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.

-
But the presentation of the results is somewhat misguided. What Shapiro ends up showing is that a local form of one of the axioms does not imply a local form of the other, which is a different thing than what one would reasonably understand is being claimed. (Anyway, without writing down precise statements of everything relevant here, the whole thing is silly.) [Off topic: Also silly is the way the negative result is established in Shapiro's book.] – Andrés Caicedo Oct 12 '13 at 15:03
Yes, I agree with that. Especially with the misguided part. It's very easy to tear this theorem away from its fragile context. This is why I mainly tried to give a vague summation of the theorem, rather than exact formulation which would require essentially reproducing a lot of the things one can find in the book. [Off topic: When are you visiting anywhere remotely reachable to a grad student without a lot of funding? (read: Europe or Israel)] – Asaf Karagila Oct 12 '13 at 15:08
(Yes, I've been thinking about it. If something comes up, naturally I'll let you know.) – Andrés Caicedo Oct 12 '13 at 15:19
(Naturally. Rumors are that YST15 might be in Israel. That sounds like a good chance!) – Asaf Karagila Oct 12 '13 at 15:26

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.

-