a characterization of OMEGA

Johan G. F. Belinfante
2008 April 1

SetDirectory["l:"]; << goedel.08mar28a; <<  tools.m

summary

The class OMEGA of all ordinal numbers is successor-invariant and closed under unions of chains.

Uchains[OMEGA]

invariant[SUCC, OMEGA]

These two properties characterize the class of ordinals.  It is shown in this notebook that the class OMEGA is the smallest successor-invariant class closed under unions of chains.  This result holds independently of the axiom of regularity.

derivation

Lemma.   (Ordinals are chains.)

SubstTest[implies, and[member[x, y], subclass[y, z]], 
        member[x, z], {y -> OMEGA, z -> chains[S]}] // 
      Reverse

or[not[member[x_, OMEGA]], 
        subclass[cart[x_, x_], union[S, inverse[S]]]] := True

Lemma.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p2, p3], p4], 
          not[implies[and[p1, p3], p4]], {p1 -> member[x, OMEGA], 
            p2 -> member[x, chains[S]], p3 -> subclass[x, y], 
            p4 -> member[U[x], Uchains[y]]}]] // Reverse

or[member[U[x_], Uchains[y_]], not[member[x_, OMEGA]], 
        not[subclass[x_, y_]]] := True

Lemma.  (For convenience, the temporary abbreviation t is used here for the least ordinal that does not belong to x.  This temporary variable is eliminated from the final statement of the lemma.)

(Map[not, 
            SubstTest[and, implies[and[p3, p4], p5], implies[p5, p7], 
              implies[and[p4, p7], p8], implies[and[p5, p8], p9], 
              not[implies[and[p3, p4], p9]], {p3 -> 
                  not[subclass[OMEGA, x]], 
                p4 -> equal[t, A[dif[OMEGA, x]]], 
                p5 -> member[t, OMEGA], p6 -> not[member[t, x]], 
                p7 -> subclass[t, OMEGA], p8 -> subclass[t, x], 
                p9 -> member[U[t], Uchains[x]]}]] // Reverse) /. 
      t -> A[dif[OMEGA, x]]

(% /. x -> x_) /. Equal -> SetDelayed

Lemma.

SubstTest[implies, equal[Uchains[x], y], 
        or[member[U[A[intersection[OMEGA, complement[x]]]], y], 
          subclass[OMEGA, x]], y -> x] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Lemma.

(Map[not, 
            SubstTest[and, implies[and[p3, p4], p5], 
              implies[and[p3, p4], p6], implies[and[p1, p3, p4], q1], 
              implies[and[p6, q1], q2], 
              not[implies[and[p1, p3, p4], q3]], {p1 -> equal[x, Uchains[x]], 
                p3 -> not[subclass[OMEGA, x]], 
                p4 -> equal[t, A[dif[OMEGA, x]]], 
                p5 -> member[t, OMEGA], p6 -> not[member[t, x]], 
                q1 -> member[U[t], x], q2 -> not[equal[U[t], t]], 
                q3 -> equal[t, succ[U[t]]]}]] /. 
          t -> A[dif[OMEGA, x]]) // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Main Theorem.  The class of ordinals is the least class that is successor-invariant and closed under unions of chains.

Map[not, 
        SubstTest[and, implies[and[p1, p3], q3], implies[and[p2, q1], q4], 
          not[implies[and[p1, p2], not[p3]]], {p1 -> 
              equal[x, Uchains[x]], p2 -> subclass[image[SUCC, x], x], 
            p3 -> not[subclass[OMEGA, x]], 
            q1 -> member[U[A[intersection[OMEGA, complement[x]]]], x], 
            q3 -> 
              equal[A[intersection[OMEGA, complement[x]]], 
                succ[U[A[intersection[OMEGA, complement[x]]]]]], 
            q4 -> 
              member[succ[U[A[intersection[OMEGA, complement[x]]]]], x]}]] // 
      Reverse

or[not[equal[x_, Uchains[x_]]], not[subclass[image[SUCC, x_], x_]], 
        subclass[OMEGA, x_]] := True

Corollary.  No set is successor-invariant and closed under unions of chains.

Map[equal[V, #] &, 
      SubstTest[class, x, 
        implies[member[x, u], 
          subclass[v, x]], {u -> 
            intersection[invar[SUCC], fix[UCHAINS]], 
          v -> OMEGA}]]

intersection[fix[UCHAINS], invar[SUCC]] := 0

comments

Smullyan and Fitting propose using this characterization to define the class of ordinals.  Doing so requires justifying the quantification over proper classes (which they discuss in detail).  Here we have avoided this difficulty by proving the characterization as a theorem.

"Raymond M. Smullyan and Melvin Fitting, Set Theory \
and the Continuum Problem, Oxford Science Publications, Clarendon Press, \
1996.  See page 64.";

Smullyan and Fitting use the suggestive term superinductive for a class that is successor-invariant and closed under unions of chains.   They also add the condition that the class hold the empty set.  This condition is redundant because it follows from the closure under chain-unions:

implies[equal[Uchains[x], x], member[0, x]]