`e0-ord-<`

is well-founded on `e0-ordinalp`

s
Major Section: MISCELLANEOUS

The soundness of ACL2 rests in part on the well-foundedness of
`e0-ord-<`

on `e0-ordinalp`

s. 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-ordinalp`

s 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)These three properties establish that(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)

`e0-ord-<`

orders the
`e0-ordinalp`

s. 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-<)))Crucially important to the proof of the well-foundedness of(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-<)))

`e0-ord-<`

on `e0-ordinalp`

s 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-ordinalp`

s 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 <.Theorem.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.

`e0-ord-<`

well-orders the `e0-ordinalp`

s. Proof. Every
infinite,` e0-ord-<`

descending sequence of `e0-ordinalp`

s 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.