The Well-Ordering Principle
===========================
For natural numbers m and n, with m > 0, consider from Java:

  n / m: number of times m goes into n without going over.
  n % m: remainder of n / m

These operators have the following properties:

  n / m, n % m in N
  n = (n / m) * m + n % m
  n % m < m

Since Java implements the Java designers must believe that
 there really are numbers n / m and n % m with the above
 properties. In other words:

  For all m, n in N, m > 0 ->
    -]q in N, -]r in N, n = qm + r /\ r < m

Should we just believe the Java designers?


Could we prove the above without the restriction that r < n? Yes.

For example, for 18 and 4: 18 = 0*4 + 18.
In general, n = 0m + n.

There are other such r's, e.g. for 18 and 4 again:
  17 = 1*4 + 14
     = 2*4 + 10
     = 3*4 + 6
     = 4*4 + 2

This suggests another characterization: perhaps the r < m is the
 smallest of all the r's. But is there a smallest? The Well-Ordering
 Principle says there is:

WOP: Suppose P is a predicate for natural numbers.
      If P is true for at least one natural number, then there is a
      smallest natural number for which it is true.

With this we prove our result.

Proof
-----
Suppose n, m in N and m > 0.
For r in N let P(r) be: there is a natural number q with n = qm + r.

[Notice that we are handling the ns and ms with a standard direct
 universal proof, not induction.
 The existential for r will be handled by the WOP inside this direct
 proof. So which predicate P is depends on m and n: we could write
 it as P_n,m to emphasize this.]

Since n = 0m + n, and 0, n in N, P is true for the number n.
By the WOP there is a smallest number for which P is true, call it s.

Suppose for contradiction that s >= m.
  Let q in N be such that n = qm + s (recall P(s) is true).
  Then n = (q+1)m + (s-m), with q+1 in N since q in N,
                            and s-m in N since s >= m.
  But this shows P(s-m) is true, contradicting that s is the smallest
   number for which P is true.

Inductive Principles
====================
We proved the following during our first proof of program correctness:

  If a_0, a_1, ... is a decreasing sequence of natural numbers then
   it is finite.

Proof
-----
Suppose not. The set of values of the sequence is non-empty (e.g. a_0
 is in it) so by the WOP it has a smallest element, occuring at some a_m.
 But then a_m+1 is smaller since the sequence is decreasing, a
 contradiction.


I state this here because it is the last of our four inductive principles.

Why do we consider the WOP and the decreasing sequence result inductive?
Because all four principles easily prove each other.

Here are two more of those 12 proofs:


WOP -> Strong Induction
-----------------------
Suppose WOP.

Let P be a predicate for natural numbers such that
  \-/n in N, (\-/k in N, k < n -> P(n))

Suppose for contradiction that P isn't always true. Then
 there is a number such that ~P is true, so by the WOP applied
 to ~P there is a smallest such number, call it s.

But then \-/k in N, k < s -> P(k), since s is the smallest
 with ~P, so P(s), a contradiction.

Induction -> No infinite decreasing sequences in N
--------------------------------------------------
Suppose Induction.

Let a_0, a_1, ... be a decreasing sequence in N.

For n in N let P(n) be a_n <= a_0 - n.
We prove P(n) for all n in N, by induction.

Base case, n = 0:
  a_0 <= a_0 - 0 = a_0 - n

Inductive Step:
  Suppose n in N and a_n <= a_0 - n (IH)
  Then a_(n+1) <  a_n, since the sequence decreases,
               <= a_0 - n, by IH for n
  So a_(n+1) <  a_0 - n. But both sides are integers, so
     a_(n+1) <= a_0 - n - 1
              = a_0 - (n + 1)

Now, if i >= a_0 then a_i <= a_0 - (n + 1)
                          <= -1 and so not in N.
Thus the sequence ends before *index* number a_0.  


The rest of the 12 equivalences are exercises.