0
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ I think your well-ordering principle even on $2$ would in fact imply LEM: given proposition $p$ define $Q(k) := (k = 0 \wedge p) \vee (k = 1)$. Then if 0 is the minimal witness for $Q$ then $p$, and if 1 is the minimal witness for $Q$ then $\lnot p$. (And in Coq, for example, the standard library defines an "accessibility" predicate inductively as the smallest subset satisfying the induction principle given above, and defines "well-ordered" as meaning every element is accessible.) $\endgroup$ – Daniel Schepler May 15 at 18:22
  • $\begingroup$ (Might you also need to add a vector of parameters $\vec t$ as input to $Q$ and prefix both with $\forall \vec t := \forall t_1 \cdots \forall t_n$, as is common in formulating for example the replacement axiom schema in ZFC?) $\endgroup$ – Daniel Schepler May 15 at 18:35
  • $\begingroup$ @DanielSchepler: I'll respond to your second comment first. You're of course right that $Q$ in the schemas would need parameters (besides the one shown) in some variants of FOL (e.g. Hilbert-style). As for your first comment, indeed well-ordering on {0,1} immediately gives LEM, and that is pretty much a special case of the explanation I gave using 3VL. The reason for looking at 3VL is that it satisfies the rule ( $¬¬Q ⊢ Q$ ) but not LEM. In any case, thanks for mentioning how "well-ordered" is defined in Coq! $\endgroup$ – user21820 May 16 at 4:45
0
$\begingroup$

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}$.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.