Well-ordering theorem and second-order logic

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.

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.