domain[ordlist[x]]

Johan G. F. Belinfante
2006 March 18

SetDirectory["l:"];  << goedel79.17a; << tools.m

summary

The class ordlist[x] is finite if and only if  x  holds finitely many ordinals, and is countably infinite otherwise.

intersection[OMEGA, x] as a wrapper

The class intersection[OMEGA, x] behaves effectively as a wrapper for classes of ordinals.  Many results are automatically recognized as true when this wrapper is used.  One can removing this wrapper to obtain equivalent statements with subclass[x, OMEGA] as an explicit hypothesis.  The following instance will be used in the sequel.

SubstTest[implies, equal[x, intersection[OMEGA, z]], 
      subclass[image[HULL[x], y], x], z -> x]

or[not[subclass[x_, OMEGA]], subclass[image[HULL[x_], y_], x_]] := 
      True

gap-free property

In this section a theorem is derived that amounts to the statement that there are no gaps between one member y of a class x of ordinals and the next hull[x, succ[y]].  Using variables, this amounts to the following statement:

Map[not, 
      SubstTest[and, implies[and[p1, r1], r3], 
        implies[and[q1, r1, r2, r3], or[r4, r5]], implies[and[r3, r5], r6], 
        implies[and[r1, r6], r7], not[and[r2, r3, r7]], 
        implies[and[q1, r3, r4], r8], 
        not[implies[and[p1, q1, r1, r2], r4]], {p1 -> subclass[x, OMEGA], 
          q1 -> member[y, OMEGA], 
r1 -> 
            member[v, x], r2 -> member[v, hull[x, succ[y]]], 
          r3 -> member[v, OMEGA], r4 -> subclass[v, y], 
          r5 -> member[y, v], r6 -> subclass[succ[y], v], 
          r7 -> subclass[hull[x, succ[y]], v], 
          r8 -> member[v, succ[y]]}]]

(% /. {x -> x_, y -> y_, v -> v_}) /. 
      Equal -> SetDelayed

Eliminating the set variable  v  yields:

Map[equal[V, #] &, 
        SubstTest[class, v, 
          or[not[member[v, x]], not[member[v, u]], not[member[y, w]], 
            not[subclass[x, w]], 
            subclass[v, y]], {u -> hull[x, succ[y]], w -> OMEGA}]] // 
      Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The following lemma will be used to eliminate the sum class functor U in the above result.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> 
          intersection[x, hull[x, succ[ord[y]]]], v -> P[ord[y]], 
        w -> id[OMEGA]}]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Removing the ord wrapper and the ordinal class wrapper, one finds:

SubstTest[implies, 
      and[equal[y, ord[z]], equal[w, intersection[OMEGA, x]]], 
      or[not[subclass[U[intersection[x, hull[x, succ[y]]]], y]], 
        subclass[intersection[w, hull[x, succ[y]]], succ[y]]], {w -> x, 
        z -> y}]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Combining these results,  one finds:

Map[not, 
      SubstTest[and, implies[and[p1, p2], p3], implies[and[p1, p2, p3], p4], 
        not[implies[and[p1, p2], p4]], {p1 -> subclass[x, OMEGA], 
          p2 -> member[y, OMEGA], 
          p3 -> subclass[U[intersection[x, hull[x, succ[y]]]], y], 
          p4 -> subclass[intersection[x, hull[x, succ[y]]], 
              succ[y]]}]]

or[not[member[y_, OMEGA]], not[subclass[x_, OMEGA]], 
        subclass[intersection[x_, hull[x_, succ[y_]]], succ[y_]]] := 
      True

a finiteness invariance

In the process of listing the ordinals in a class in increasing order, each time one adds only one more member, and so at any stage of the iteration, only finitely many have been listed.  A formal statement that this finiteness property is an invariance of the iteration process is derived in this section.  The basic idea is this:

SubstTest[implies, and[subclass[u, v], member[v, FINITE]], 
      member[u, 
        FINITE], 
{u -> 
          intersection[x, hull[x, succ[y]]], 
        v -> intersection[x, succ[y]]}]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Applying the result of the preceding section yields:

Map[not, 
      SubstTest[and, implies[and[p1, p2], p4], implies[and[p1, p4], p5], 
        implies[and[p2, p3], p6], implies[and[p5, p6], p7], 
        not[implies[and[p1, p2, p3], p7]], {p1 -> subclass[x, OMEGA], 
          p2 -> member[y, x], 
          p3 -> member[intersection[x, y], FINITE], 
          p4 -> member[y, OMEGA], 
p5 -> 
            subclass[intersection[x, hull[x, succ[y]]], succ[y]], 
          p6 -> member[intersection[x, succ[y]], FINITE], 
          p7 -> member[intersection[x, hull[x, succ[y]]], 
              FINITE]}]]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The variable  y  is eliminated now to obtain:

Map[implies[not[member[x, FINITE]], equal[V, #]] &, 
        SubstTest[class, y, 
          implies[and[subclass[x, u], member[y, v]], 
            member[intersection[x, hull[x, succ[y]]], w]], {u -> OMEGA, 
            v -> intersection[x, image[inverse[IMAGE[id[x]]], FINITE]], 
            w -> FINITE}]] // Reverse

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

The inverse images can be eliminated using:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], 
{u -> y, 
        v -> image[inverse[HULL[x]], image[inverse[IMAGE[id[x]]], z]], 
        w -> composite[IMAGE[id[x]], HULL[x]]}]

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], 
{p1 -> 
            and[subclass[x, OMEGA], not[member[x, FINITE]]], 
          p2 -> subclass[
              image[SUCC, 
                intersection[x, image[inverse[IMAGE[id[x]]], FINITE]]], 
              image[inverse[HULL[x]], 
                image[inverse[IMAGE[id[x]]], 
                  FINITE]]], 
p3 -> 
            subclass[
              image[IMAGE[id[x]], 
                image[HULL[x], 
                  image[SUCC, 
                    intersection[x, image[inverse[IMAGE[id[x]]], FINITE]]]]], 
              FINITE]}]]

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

using the invariance

If  v is a subclass of a class w that is invariant under  u, then range[iterate[u,v]] is a subclass of w.  For the special case that  u  is the function that produces the next ordinal in a class  x, this says:

Map[or[not[member[A[intersection[OMEGA, x]], w]], #] &, 
      SubstTest[implies, and[subclass[v, w], invariant[u, w]], 
        subclass[range[iterate[u, v]], 
          w], 
{u -> 
            composite[HULL[intersection[OMEGA, x]], SUCC], 
          v -> set[A[intersection[OMEGA, x]]]}]]

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Removing the ordinal-class wrapper yields:

SubstTest[implies, 
      and[equal[y, intersection[OMEGA, x]], member[A[y], w], 
        invariant[composite[HULL[y], SUCC], w]], 
      subclass[range[ordlist[x]], w], y -> x]

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

The class that was shown to be invariant in the preceding section is  w = intersection[x,image[inverse[IMAGE[id[x]]], FINITE]].  One obtains in this case:

SubstTest[or, not[member[A[x], w]], not[subclass[x, OMEGA]], 
      not[subclass[image[HULL[x], image[SUCC, w]], w]], 
      subclass[range[ordlist[x]], w], 
      w -> intersection[x, image[inverse[IMAGE[id[x]]], FINITE]]]

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

This simplifies greatly when  x  is infinite. If  x  is an infinite class of ordinals, then intersection[x,y] is finite for every y listed by ordlist[x].

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        implies[p1, p4], implies[p1, p5], implies[p1, p6], implies[p6, p7], 
        implies[p1, p8], implies[and[p2, p3, p4, p5, p7, p8], p9], 
        not[implies[p1, p9]], {p1 -> 
            and[subclass[x, OMEGA], not[member[x, FINITE]]], 
          p2 -> not[equal[0, x]], 
          p3 -> member[A[x], x], 
p4 -> 
            subclass[
              image[HULL[x], 
                image[SUCC, 
                  intersection[x, image[inverse[IMAGE[id[x]]], FINITE]]]], 
              x], 
p5 -> 
            subclass[
              image[IMAGE[id[x]], 
                image[HULL[x], 
                  image[SUCC, 
                    intersection[x, image[inverse[IMAGE[id[x]]], FINITE]]]]], 
              FINITE], p6 -> disjoint[x, A[x]], 
          p7 -> member[intersection[x, A[x]], FINITE], 
          p8 -> subclass[x, OMEGA], 
          p9 -> subclass[image[IMAGE[id[x]], range[ordlist[x]]], 
              FINITE]}]]

or[member[x_, FINITE], not[subclass[x_, OMEGA]], 
        subclass[image[IMAGE[id[x_]], range[ordlist[x_]]], FINITE]] := 
      True

an important corollary

The condition derived in the preceding section implies that if  x  is an infinite class of ordinals, then the range of ordlist[x] is contained in  U[x].

Map[not, 
        SubstTest[and, implies[p0, p3], implies[p1, p2], 
          implies[and[p0, p1, p2, p3], p4], 
          not[implies[and[p0, p1], p4]], {p0 -> 
              equal[y, range[ordlist[x]]], 
            p1 -> and[subclass[x, OMEGA], not[member[x, FINITE]]], 
            p2 -> subclass[image[IMAGE[id[x]], range[ordlist[x]]], FINITE], 
            p3 -> subclass[y, x], p4 -> subclass[y, U[x]]}]] /. 
      y -> range[ordlist[x]]

or[member[x_, FINITE], not[subclass[x_, OMEGA]], 
        subclass[range[ordlist[x_]], U[x_]]] := True

Reintroducing the ordinal class wrapper yields:

SubstTest[implies, and[subclass[y, OMEGA], not[member[y, FINITE]]], 
      subclass[range[ordlist[y]], U[y]], 
      y -> intersection[OMEGA, x]]

or[member[intersection[OMEGA, x_], FINITE], 
        subclass[range[ordlist[x_]], U[intersection[OMEGA, x_]]]] := 
      True

applying induction

The recursion relation for ordlist[x] is used to derive a temporary rewrite rule:

IminComp[ordlist[x], SUCC, V]

image[inverse[ordlist[x_]], U[intersection[OMEGA, x_]]] := 
      image[inverse[SUCC], domain[ordlist[x]]]

From this one derives the fact that if the set of ordinals listed by ordlist is contained in U[intersection[OMEGA,x]], then the list goes on forever.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> range[ordlist[x]], 
        v -> U[intersection[OMEGA, x]], 
        w -> inverse[ordlist[x]]}]

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

It was shown in the preceding section that this is the case when  x  holds an infinite number of ordinals.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], 
{p1 -> 
            not[member[intersection[OMEGA, x], FINITE]], 
          p2 -> subclass[range[ordlist[x]], 
              U[intersection[OMEGA, x]]], 
p3 -> 
            invariant[SUCC, domain[ordlist[x]]]}]]

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

An application of induction yields:

SubstTest[implies, INDUCTIVE[w], subclass[omega, w], 
      w -> domain[ordlist[x]]]

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

A more precise statement is that if  x  holds infinitely many ordinals then the domain of ordlist[x] is equal to omega.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p1, p3], 
        implies[and[p2, p3], p4], implies[p4, p5], implies[p5, p6], 
        not[implies[p1, p6]], {p1 -> 
            not[member[intersection[OMEGA, x], FINITE]], 
          p2 -> 
            not[empty[intersection[OMEGA, x]]], 
p3 -> 
            invariant[SUCC, domain[ordlist[x]]], 
          p4 -> subclass[omega, domain[ordlist[x]]], 
          p5 -> not[member[domain[ordlist[x]], omega]], 
          p6 -> equal[domain[ordlist[x]], omega]}]]

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

two rewrite rules for domain[ordlist[x]]

If  x  only holds finitely many ordinals, then the domain of ordlist[x] is a natural number.

SubstTest[implies, member[y, FINITE], 
      member[domain[ordlist[y]], omega], 
      y -> intersection[OMEGA, x]]

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

The converse also holds.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], {p1 -> member[domain[ordlist[x]], omega], 
          p2 -> not[equal[domain[ordlist[x]], omega]], 
          p3 -> member[intersection[OMEGA, x], FINITE]}]]

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

Since the implications go in both directions, one can introduce a rewrite rule.

equiv[member[domain[ordlist[x]], omega], 
      member[intersection[OMEGA, x], FINITE]]

member[domain[ordlist[x_]], omega] := 
      member[intersection[OMEGA, x], FINITE]

It obviously follows that in this case the domain of ordlist[x] is not the set omega.

SubstTest[implies, equal[omega, z], not[member[z, omega]], 
      z -> domain[ordlist[x]]]

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

This yields a rewrite for the case that the domain of ordlist[x] is omega.

equiv[equal[domain[ordlist[x]], omega], 
      not[member[intersection[OMEGA, x], FINITE]]]

equal[omega, domain[ordlist[x_]]] := 
      not[member[intersection[OMEGA, x], FINITE]]