o<is well-founded on
Major Section: MISCELLANEOUS
The soundness of ACL2 rests in part on the well-foundedness of
o-ps. 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
o< is well-founded on
having to assert any connection to the ordinals and that is what we do here.
books/ordinals/proof-of-well-foundedness carries out the proof
outlined below in ACL2, using only that the natural numbers are
Before outlining the above mentioned proof, we note that in the analogous
documentation page of ACL2 Version_2.7, there is a proof of the
e0-ordinalps, the less-than relation
and recognizer for the old ordinals (that is, for the ordinals appearing in
ACL2 up through that version). Manolios and Vroon have given a proof in ACL2
Version_2.7 that the current ordinals (based on
order-isomorphic to the old ordinals (based on
e0-ordinalp). Their proof establishes that switching from the old
ordinals to the current ordinals preserves the soundness of ACL2. For
details see their paper:
Manolios, Panagiotis & Vroon, Daron. Ordinal arithmetic in ACL2. Kaufmann, Matt, & Moore, J Strother (eds). Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July, 2003. See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.
We now give an outline of the above mentioned proof of well-foundedness. We
first observe three facts about
o< on ordinals that have been proved by
ACL2 using only structural induction on lists. These theorems can be proved
(defthm transitivity-of-o< (implies (and (o< x y) (o< y z)) (o< x z)) :rule-classes nil)These three properties establish that
(defthm non-circularity-of-o< (implies (o< x y) (not (o< y x))) :rule-classes nil)
(defthm trichotomy-of-o< (implies (and (o-p x) (o-p y)) (or (equal x y) (o< x y) (o< y x))) :rule-classes nil)
o-ps. To put such a statement in the most standard mathematical nomenclature, we can define the macro:
(defmacro o<= (x y) `(not (o< ,y ,x)))and then establish that
o<=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-o<= (implies (and (o-p x) (o-p y) (o<= x y) (o<= y x)) (equal x y)) :rule-classes nil :hints (("Goal" :use non-circularity-of-o<)))Crucially important to the proof of the well-foundedness of
(defthm transitivity-of-o<= (implies (and (o-p x) (o-p y) (o<= x y) (o<= y z)) (o<= x z)) :rule-classes nil :hints (("Goal" :use transitivity-of-o<)))
(defthm trichotomy-of-o<= (implies (and (o-p x) (o-p y)) (or (o<= x y) (o<= y x))) :rule-classes nil :hints (("Goal" :use trichotomy-of-o<)))
o-ps is the concept of ordinal-depth, abbreviated
(defun od (l) (if (o-finp l) 0 (1+ (od (o-first-expt l)))))If the
xis smaller than that of an
(defun od-1 (x y) (if (o-finp x) (list x y) (od-1 (o-first-expt x) (o-first-expt y))))Remark. A consequence of this lemma is the fact that if
(defthm od-implies-ordlessp (implies (and (o-p x) (< (od x) (od y))) (o< x y)) :hints (("Goal" :induct (od-1 x y))))
s = s(1),
s(2), ... is an infinite,
o<descending sequence of
od(s(2)), ... is a ``weakly'' descending sequence of non-negative integers:
od(s(i))is greater than or equal to
Lemma Main. For each non-negative integer
the set of
od less than or equal to
Base Case. n = 0. The o-ps with 0 od are the non-negative integers. On the non-negative integers, o< is the same as <.Theorem.
Induction Step. n > 0. We assume that o< well-orders the o-ps with od less than n.
If o< does not well-order the o-ps with od less than or equal to n, consider, D, the set of infinite, o< descending sequences of o-ps of od less than or equal to n. The first element of a sequence in D has od n. Therefore, the o-first-expt of the first element of a sequence in D has od n-1. Since o<, by IH, well-orders the o-ps with od less than n, the set of o-first-expts 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 minimum integer such that for some infinite, o< descending sequence s of o-ps with od less than or equal to n, the first element of s has an o-first-expt of B and an o-first-coeff of k. Notice that k is positive.
Having fixed B and k, let s = s(1), s(2), ... be an infinite, o< descending sequence of o-ps with od less than or equal to n such that s(1) has a o-first-expt of B and an o-first-coeff of k.
We show that each s(i) has a o-first-expt of B and an o-first-coeff of k. For suppose that s(j) is the first member of s either with o-first-expt B and o-first-coeff m (m neq k) or with o-first-expt B' and o-first-coeff B' (B' neq B). If (o-first-expt s(j)) = B', then B' has od n-1 (otherwise, by IH, s would not be infinite) and B' is o< 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; but this contradicts the fact that s is descending.
Thus, by the definition of o<, for s to be a decreasing sequence of o-ps, (o-rst s(1)), (o-rst s(2)), ... must be a decreasing sequence. We end by showing this cannot be the case. Let t = t(1), t(2), ... be an infinite sequence of o-ps such that t(i) = (o-rst s(i)). Then t is infinitely descending. Furthermore, t(1) begins with an o-p B' that is o< 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.
o-ps. Proof. Every infinite,
o<descending sequence of
o-ps has the property that each member has
odless than or equal to the
n, of the first member of the sequence. This contradicts Lemma Main. Q.E.D.