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.