PROOF-OF-WELL-FOUNDEDNESS

a proof that e0-ord-< is well-founded on e0-ordinalps
Major Section:  MISCELLANEOUS

The soundness of ACL2 rests in part on the well-foundedness of e0-ord-< on e0-ordinalps. This can be taken as obvious if one is willing to grant that those concepts are simply encodings of the standard mathematical notions of the ordinals below epsilon-0 and its natural ordering relation. But it is possible to prove that e0-ord-< is well-founded on e0-ordinalps without having to assert any connection to the ordinals and that is what we do here.

We first observe three facts about e0-ord-< on ordinals that have been proved by ACL2 using only structural induction on lists. These theorems can be proved by hand.

(defthm transitivity-of-e0-ord-<
  (implies (and (e0-ord-< x y)
                (e0-ord-< y z))
           (e0-ord-< x z))
  :rule-classes nil)

(defthm non-circularity-of-e0-ord-< (implies (e0-ord-< x y) (not (e0-ord-< y x))) :rule-classes nil)

(defthm trichotomy-of-e0-ord-< (implies (and (e0-ordinalp x) (e0-ordinalp y)) (or (equal x y) (e0-ord-< x y) (e0-ord-< y x))) :rule-classes nil)

These three properties establish that e0-ord-< orders the e0-ordinalps. To put such a statement in the most standard mathematical nomenclature, we can define the function:
(defun e0-ord-<= (x y)
  (or (equal x y) (e0-ord-< x y)))
and then establish that e0-ord-<= is a relation that is a simple, complete (i.e., total) order on ordinals by the following three lemmas, which have been proved:
(defthm antisymmetry-of-e0-ord-<=
  (implies (and (e0-ordinalp x)
                (e0-ordinalp y)
                (e0-ord-<= x y)
                (e0-ord-<= y x))
           (equal x y))
  :rule-classes nil
  :hints (("Goal" :use non-circularity-of-e0-ord-<)))

(defthm transitivity-of-e0-ord-<= (implies (and (e0-ord-<= x y) (e0-ord-<= y z)) (e0-ord-<= x z)) :rule-classes nil :hints (("Goal" :use transitivity-of-e0-ord-<)))

(defthm trichotomy-of-e0-ord-<= (implies (and (e0-ordinalp x) (e0-ordinalp y)) (or (e0-ord-<= x y) (e0-ord-<= y x))) :rule-classes nil :hints (("Goal" :use trichotomy-of-e0-ord-<)))

Crucially important to the proof of the well-foundedness of e0-ord-< on e0-ordinalps is the concept of ordinal-depth, abbreviated od:
(defun od (l) (if (atom l) 0 (1+ (od (car l)))))
If the od of an e0-ordinalp x is smaller than that of an e0-ordinalp y, then x is e0-ord-< y:
(defthm od-implies-ordlessp
  (implies (< (od x) (od y))
           (e0-ord-< x y)))
Remark. A consequence of this lemma is the fact that if s = s(1), s(2), ... is an infinite, e0-ord-< descending sequence, then od(s(1)), od(s(2)), ... is a ``weakly'' descending sequence of non-negative integers: od(s(i)) is greater than or equal to od(s(i+1)).

Lemma Main. For each non-negative integer n, e0-ord-< well-orders the set of e0-ordinalps with od less than or equal to n .

 Base Case.  n = 0.  The e0-ordinalps with 0 od are the non-negative
 integers.  On the non-negative integers, e0-ord-< is the same as <.

Induction Step. n > 0. We assume that e0-ord-< well-orders the e0-ordinalps with od less than n.

If e0-ord-< does not well-order the e0-ordinalps with od less than or equal to n, consider, D, the set of infinite, e0-ord-< descending sequences of e0-ordinalps of od less than or equal to n. The first element of a sequence in D has od n. Therefore, the car of the first element of a sequence in D has od n-1. Since e0-ord-<, by IH, well-orders the e0-ordinalps with od less than n, the set of cars of first elements of the sequences in D has a minimal element, which we denote by B and which has od of n-1.

Let k be the least integer such that for some infinite, e0-ord-< descending sequence s of e0-ordinalps with od less than or equal to n, the first element of s begins with k occurrences of B but not k+1 occurrences of B. Notice that k is positive.

Having fixed B and k, let s = s(1), s(2), ... be an infinite, e0-ord-< descending sequence of e0-ordinalps with od less than or equal to n such that B occurs exactly k times at the beginning of s(1).

B occurs exactly k times at the beginning of each s(i). For suppose that s(j) is the first member of s with exactly m occurrences of B at the beginning, m /= k. If m = 0, then the car of s(j) has od n-1 (otherwise, by IH, s would not be infinite) and the car of s(j) is e0-ord-< B, contradicting the minimality of B. If 0 < m < k, then the fact that the sequence beginning at s(j) is infinitely descending contradicts the minimality of k. If m > k, then s(j) is greater than its predecessor, which has only k occurrences of B at the beginning; but this contradicts the fact that s is descending.

Let t = t(1), t(2), ... be the sequence of e0-ordinalps that is obtained by letting t(i) be the result of removing B from the front of s(i) exactly k times. t is infinitely descending. Furthermore, t(1) begins with an e0-ordinalp B' that is e0-ord-< B. Since t is in D, t(1) has od n, therefore, B' has od n-1. But this contradicts the minimality of B. Q.E.D.

Theorem. e0-ord-< well-orders the e0-ordinalps. Proof. Every infinite, e0-ord-< descending sequence of e0-ordinalps has the property that each member has od less than or equal to the od, n, of the first member of the sequence. This contradicts Lemma Main. Q.E.D.