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?
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,<)$:
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$:
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}$.