Disparity between Induction and Well-ordering Principles Over classical logic, the induction and well-ordering schemas are equivalent. These schemas state the following, given any linear ordering $(W,<)$ and property $Q$ on $W$:

Induction: $∀k{∈}W\ ( \ ∀i{∈}W_{<k}\ ( \ Q(i) \ ) ⇒ Q(k) \ ) ⇒ ∀k{∈}W\ ( \ Q(k) \ )$.
Well-ordering: $∃k{∈}W\ ( \ Q(k) \ ) ⇒ ∃k{∈}W\ ( \ Q(k) ∧ ∀i{∈}W_{<k}\ ( \ ¬Q(i) \ ) \ )$.

When applied to the ordering on $\mathbb{N}$, these yield the (so-called) "strong induction" schema and the "well-ordering principle". It sometimes seems as though the latter gives a quicker proof, but on the other hand proofs based on just induction feel more direct. Is there any substance to this feeling? Can non-classical logics illuminate the disparity between these two principles, and explain why they feel different even in ordinary mathematics?
 A: The equivalence between induction and well-ordering breaks down in the absence of LEM (law of excluded middle). To isolate the reliance on LEM, consider the corresponding Fitch-style rules over Kleene's 3-valued logic 3VL for any given linear order $(W,<)$:

Induction rule: $∀k{∈}W\ ( \ ∀i{∈}W_{<k}\ ( Q(i) ) ⊢ Q(k) \ ) ⊢ ∀k{∈}W\ ( \ Q(k) \ )$.
Well-ordering rule: $∃k{∈}W\ ( \ Q(k) \ ) ⊢ ∃k{∈}W\ ( \ Q(k) ∧ ∀i{∈}W_{<k}\ ( ¬Q(i) ) \ )$.

Note for induction on $(\mathbb{N},<)$, the induction rule is equivalent over 3VL to the basic induction rule (i.e. "$Q(0) ∧ ∀k{∈}\mathbb{N}\ ( \ Q(k)⊢Q(k+1) \ ) ⊢ ∀k{∈}\mathbb{N}\ ( \ Q(k) \ )$" for each property $Q$ on $\mathbb{N}$). But these are very different from the well-ordering rule even for $\mathbb{N}$.
The induction rule is sound over 3VL if $(W,<)$ is truly a well-order, and we can easily observe this fact by transfinite induction in the (classical) meta-system. But the well-ordering rule is not sound over 3VL even if $(W,<)$ is a well-order, because it may be that for some $k,m∈W$ we have $k<m$ and $Q(k) ≡ \text{null}$ but $Q(m) ≡ \text{true}$.
So there is a logically significant disparity between these two principles. Intuitively, well-ordering generates more information than induction.
Furthermore, induction on $\mathbb{N}$ is intuitionistically sound in the sense that every instance is witnessed by a program as per the BHK interpretation. In contrast, well-ordering on $\mathbb{N}$ is not intuitionistically sound, because if $Q(k,x)$ says "there is a program that has length $k$ and outputs string $x$", then any program witnessing "$∀x{∈}\mathbb{N}\ ( \ ∃k{∈}\mathbb{N}\ ( \ Q(k,x) \ ) ⇒ ∃k{∈}\mathbb{N}\ ( \ Q(k,x) ∧ ∀i{∈}\mathbb{N}_{<k}\ ( ¬Q(i,x) ) \ ) \ )$" can be used to compute Kolmogorov complexity, which is impossible.
This disparity actually shows up in a wide variety of mathematical problems. For example, any proof that Kolmogorov complexity is well-defined requires LEM as shown above, and is trivial via well-ordering on $\mathbb{N}$. Another example is the proof that every positive integer $n > 1$ is not a factor of $2^n-1$:

Take any positive integer $n > 1$ such that $n \mid 2^n-1$. Let $p$ be the smallest prime factor of $n$, which exists by well-ordering on $\mathbb{N}$ since $n$ has a prime factor, and let $k$ be the positive integer such that $p·k = n$. Then $p \mid 2^n-1$. Note that $p \nmid 2$ since $2 \nmid 2^n-1$, and so $2^{p-1} ≡ 1 \pmod{p}$ by Fermat's little theorem. Thus $1 ≡ 2^n ≡ (2^p)^k ≡ 2^k \pmod{p}$. Let $c$ be the minimum positive integer such that $2^c ≡ 1 \pmod{p}$, again by well-ordering on $\mathbb{N}$. Then $c > 1$ and $c \mid k , p-1$ (otherwise by the division lemma and Euclid's lemma we can obtain a contradiction). Now let $q$ be the smallest prime factor of $c$, yet again by well-ordering on $\mathbb{N}$. Thus $q \mid c \mid k,p-1$, and hence $q$ is a prime factor of $n$ that is smaller than $p$, contradicting minimality of $p$.

Classically, every proof using well-ordering can be mechanically translated into a proof using only induction, but as the above examples illustrate, well-ordering sometimes seems to 'generate' more information, and this extra information is actually coming from LEM. It feels especially unnatural to use induction instead of well-ordering in the number theory example above, because the intrinsic structure of the problem does not follow the structure of the natural ordering on $\mathbb{N}$.
