reify rule for enum[x]

Johan G. F. Belinfante
2010 December 13

SetDirectory["l:"];  << goedel.10dec11a

summary

The image by  enum[x]  of any ordinal  α  belonging to its domain is  Ω ⋂ x  ⋂  APPLY[enum[x], α].   The class of all ranges of partial enumerations of the ordinals in a class  x  is the class of all intersections of  x  with ordinals.   The class of all partial enumerations of the ordinals in a class  x  is the class of enumerations whose ranges are intersections of  x  with ordinals.   These results are used to derive reify rules for partenum and enum.

a formula for image[enum[x], y]

At any point in the enumeration of ordinals in a class x, the set of ordinals already listed is the set of all ordinals less that the next one to be listed.  This observation will be given a formal statement in this section.

Observation.  An inclusion in one direction is already available:

subclass[image[enum[x], y], 
      intersection[OMEGA, x, APPLY[enum[x], y]]]

To obtain an inclusion in the reverse direction, one has only to eliminate a variable.

Lemma.

Map[equal[V, #] &, 
      SubstTest[class, u, 
        implies[and[member[y, w], member[u, z]], 
          member[u, y]], {w -> domain[enum[x]], 
          z -> image[inverse[enum[x]], 
              intersection[OMEGA, x, APPLY[enum[x], y]]]}]]

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

Combining this inclusion with the reverse inclusion yields an equation, the main result of this section.

Main Theorem.   A formula for image[enum[x], y]  for  y ∈ domain[enum[x]].

SubstTest[and, implies[p, subclass[u, v]], 
      subclass[v, u], {p -> member[y, domain[enum[x]]], 
        u -> intersection[OMEGA, x, APPLY[enum[x], y]], 
        v -> image[enum[x], y]}]

or[equal[image[enum[x_], y_], 
          intersection[OMEGA, x_, APPLY[enum[x_], y_]]], 
        not[member[y_, domain[enum[x_]]]]] := True

In order to eliminate the variable  y here it is convenient to restate this result as a simple equation by introducing an image[V, - ] term for the condition  y ∈ domain[enum[x]].

Corollary.   Restatement of the main result.

equal[
      intersection[OMEGA, x, APPLY[enum[x], y], 
        image[V, intersection[domain[enum[x]], set[y]]]], 
      intersection[image[V, intersection[domain[enum[x]], set[y]]], 
        image[enum[x], y]]]

intersection[OMEGA, x_, APPLY[enum[x_], y_], 
        image[V, intersection[domain[enum[x_]], set[y_]]]] := 
      intersection[image[V, intersection[domain[enum[x]], set[y]]], 
        image[enum[x], y]]

The variable  y  can now be eliminated using reify.

Theorem.

Map[composite[VERTSECT[#], id[domain[enum[x]]]] &, 
      SubstTest[reify, y, 
        intersection[OMEGA, x, APPLY[t, y], 
          image[V, intersection[domain[t], set[y]]]], 
        t -> enum[x]]]

composite[IMAGE[id[intersection[OMEGA, x_]]], enum[x_]] := 
      composite[IMAGE[enum[x]], id[domain[enum[x]]]]

Corollary.   A slightly simpler equation of the same type as the previous one.

Assoc[IMAGE[id[x]], IMAGE[id[OMEGA]], enum[x]]

composite[IMAGE[id[x_]], enum[x_]] := 
      composite[IMAGE[enum[x]], id[domain[enum[x]]]]

a general result

In this section a corollary is derived that has does not mention enumerations, but follows from the results obtained above.

Lemma.

Map[equal[intersection[OMEGA, x], fix[#]] &, 
      Assoc[composite[HULL[intersection[OMEGA, x]], 
          IMAGE[id[intersection[OMEGA, x]]]], enum[x], 
        inverse[enum[x]]]]

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

Theorem.

SubstTest[implies, equal[t, intersection[x, OMEGA]], 
        subclass[t, fix[composite[HULL[t], IMAGE[id[x]]]]], t -> x] // 
      Reverse

or[not[subclass[x_, OMEGA]], 
        subclass[x_, fix[composite[HULL[x_], IMAGE[id[x_]]]]]] := 
      True

ranges of partial enumerations

Returning to the theory of enumeration, in this section some groundwork is laid down to prepare for the derivation of a formula for the class of all ranges of partial enumerations.  The general idea here is to write any partial enumeration as the co-restriction of enum[x] to an ordinal, starting with the known fact that any partial enumeration is the restriction of enum[x] to an ordinal.  If that ordinal is in the domain of enum[x], then applying enum[x] to that ordinal yields another ordinal that can be used to write the partial enumeration as a co-restriction to an ordinal.

Lemma.  (Removing an ord wrapper.)

SubstTest[implies, equal[y, ord[t]], 
        member[composite[id[y], enum[x]], ENUMS], t -> y] // 
      Reverse

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

Lemma.

SubstTest[implies, member[y, OMEGA], 
        member[composite[id[y], enum[x]], ENUMS], 
        y -> APPLY[enum[x], ord[y]]] // Reverse

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

Lemma.

SubstTest[implies, 
        and[member[u, ENUMS], member[v, ENUMS], equal[range[u], range[v]]], 
        equal[u, v], {u -> composite[enum[x], id[ord[y]]], 
          v -> composite[id[APPLY[enum[x], ord[y]]], enum[x]]}] // 
      Reverse

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

Theorem.  Rewriting a restriction of enum[x] to an ordinal as a co-restriction.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], p4], 
          not[implies[p1, p4]], {p1 -> member[ord[y], domain[enum[x]]], 
            p2 -> equal[image[enum[x], ord[y]], 
                intersection[OMEGA, x, APPLY[enum[x], ord[y]]]], 
            p3 -> 
              member[composite[id[APPLY[enum[x], ord[y]]], enum[x]], ENUMS], 
            p4 -> equal[composite[enum[x], id[ord[y]]], 
                composite[id[APPLY[enum[x], ord[y]]], enum[x]]]}]] // 
      Reverse

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

Corollary.   (Remove the ord wrappers.)

SubstTest[implies, equal[y, ord[t]], 
        or[equal[composite[enum[x], id[y]], 
            composite[id[APPLY[enum[x], y]], enum[x]]], 
          not[member[y, domain[enum[x]]]]], t -> y] // 
      Reverse

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

There are two cases to be considered, depending on whether or not the class of ordinals in  x  is a set or a proper class.

Lemma.  (The case of a set.)

SubstTest[implies, 
        and[member[u, OMEGA], member[v, OMEGA], subclass[u, v]], 
        or[equal[u, v], member[u, v]], v -> domain[enum[x]]] // 
      Reverse

(% /. {u -> u_, x -> x_}) /. 
      Equal -> SetDelayed

Lemma.  (The case of a proper class.)

SubstTest[implies, 
        and[member[u, OMEGA], equal[v, OMEGA], subclass[u, v]], member[u, v], 
        v -> domain[enum[x]]] // Reverse

(% /. {u -> u_, x -> x_}) /. 
      Equal -> SetDelayed

The next lemma combines the two cases considered in the preceding two lemmas.

Lemma.

Map[not, 
        SubstTest[and, implies[p1, or[p2, p3, p4]], implies[and[p1, p3], p4], 
          not[implies[p1, or[p2, p4]]], {p1 -> 
              and[member[u, OMEGA], subclass[u, domain[enum[x]]]], 
            p2 -> equal[u, domain[enum[x]]], 
            p3 -> not[member[intersection[OMEGA, x], V]], 
            p4 -> member[u, domain[enum[x]]]}]] // Reverse

(% /. {u -> u_, x -> x_}) /. 
      Equal -> SetDelayed

Lemma.  A simplification rule.

ImageComp[IMAGE[id[x]], IMAGE[id[OMEGA]], OMEGA]

image[IMAGE[id[intersection[OMEGA, x_]]], OMEGA] := 
      image[IMAGE[id[x]], OMEGA]

Theorem.  A condition for membership in the class  image[IMAGE[id[x]], Ω].

(SubstTest[or, 
            member[intersection[z, t], image[IMAGE[id[z]], OMEGA]], 
            not[member[t, OMEGA]], t -> APPLY[enum[z], domain[t]]]) /. 
        z -> intersection[OMEGA, x] // Reverse

(% /. {x -> x_, t -> t_}) /. 
      Equal -> SetDelayed

Technical Lemma    (This is needed shortly to get around equality substitution limitations in the GOEDEL program.)

SubstTest[implies, equal[t, w], equal[range[t], range[w]], 
        w -> composite[id[APPLY[enum[x], domain[t]]], enum[x]]] // 
      Reverse

(% /. {x -> x_, t -> t_}) /. 
      Equal -> SetDelayed

breakup into two cases

Theorem.  The two cases.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p2, p4], 
          implies[and[p3, p4], or[p5, p6]], 
          not[implies[p1, or[p5, p6]]], {p1 -> member[t, partenum[x]], 
            p2 -> equal[t, composite[enum[x], id[domain[t]]]], 
            p3 -> member[domain[t], OMEGA], 
            p4 -> subclass[domain[t], domain[enum[x]]], 
            p5 -> member[domain[t], domain[enum[x]]], 
            p6 -> equal[domain[t], domain[enum[x]]]}]] // 
      Reverse

or[equal[domain[t_], domain[enum[x]]], 
        member[domain[t_], domain[enum[x_]]], not[member[t_, partenum[x_]]]] := 
      True

In the easy case that  domain[t] = domain[enum[x]], one has t = enum[x].

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p3], implies[and[p1, p2, p3], p4], 
          not[implies[and[p1, p2], p4]], {p1 -> member[t, partenum[x]], 
            p2 -> equal[domain[t], domain[enum[x]]], 
            p3 -> equal[t, composite[enum[x], id[domain[t]]]], 
            p4 -> equal[t, enum[x]]}]] // Reverse

or[equal[t_, enum[x_]], not[equal[domain[t_], domain[enum[x_]]]], 
        not[member[t_, partenum[x_]]]] := True

Lemma.  A simplification rule.

equal[intersection[x, tc[x]], x]

intersection[x_, tc[x_]] := x

Lemma.

(SubstTest[implies, member[t, OMEGA], 
            member[intersection[t, w], image[IMAGE[id[w]], OMEGA]], 
            t -> tc[w]] // Reverse) /. 
      w -> intersection[OMEGA, x]

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

Theorem.   The easy case.

Map[not, 
        SubstTest[and, implies[and[p1, p2], p3], implies[and[p1, p3], p4], 
          not[implies[and[p1, p2], p4]], {p1 -> member[t, partenum[x]], 
            p2 -> equal[domain[t], domain[enum[x]]], 
            p3 -> equal[t, enum[x]], 
            p4 -> member[range[t], image[IMAGE[id[x]], OMEGA]]}]] // 
      Reverse

(% /. {x -> x_, t -> t_}) /. 
      Equal -> SetDelayed

the second case

The following proof step is omitted in the next lemma:  implies[and[p8, p9, p10], p11].

Lemma.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p2, p5], p7], 
          implies[and[p2, p7], p8], implies[p5, p9], implies[p8, p10], 
          not[implies[and[p1, p5], p11]], {p1 -> member[t, partenum[x]], 
            p2 -> equal[t, composite[enum[x], id[domain[t]]]], 
            p5 -> member[domain[t], domain[enum[x]]], 
            p7 -> 
              equal[composite[enum[x], id[domain[t]]], 
                composite[id[APPLY[enum[x], domain[t]]], enum[x]]], 
            p8 -> equal[t, 
                composite[id[APPLY[enum[x], domain[t]]], enum[x]]], 
            p9 -> member[intersection[OMEGA, x, APPLY[enum[x], domain[t]]], 
                image[IMAGE[id[x]], OMEGA]], 
            p10 -> 
              equal[range[t], 
                intersection[OMEGA, x, APPLY[enum[x], domain[t]]]], 
            p11 -> member[range[t], image[IMAGE[id[x]], OMEGA]]}]] // 
      Reverse

(% /. {t -> t_, x -> x_}) /. 
      Equal -> SetDelayed

Combine the two cases.

Main Theorem.  If  t  is a partial enumeration of the ordinals in  x, then the range of  t  is the intersection of  x  with an ordinal.

Map[not, 
        SubstTest[and, implies[p1, or[p5, p6]], 
          not[implies[p1, p11]], {p1 -> member[t, partenum[x]], 
            p5 -> member[domain[t], domain[enum[x]]], 
            p6 -> equal[domain[t], domain[enum[x]]], 
            p11 -> member[range[t], image[IMAGE[id[x]], OMEGA]]}]] // 
      Reverse

or[member[range[t_], image[IMAGE[id[x_]], OMEGA]], 
        not[member[t_, partenum[x_]]]] := True

Theorem.   Eliminate the variable  t.

Map[
      equal[V, #] &, dif[partenum[x], 
            image[inverse[IMAGE[SECOND]], image[IMAGE[id[x]], OMEGA]]] // 
          complement // Normality]

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

The reverse inclusion is already available.

Main Theorem.  The class of ranges of the partial enumerations of a class  x   is the class of all intersections of  x  with ordinals.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> image[IMAGE[SECOND], partenum[x]], 
        v -> image[IMAGE[id[x]], OMEGA]}]

image[IMAGE[SECOND], partenum[x_]] := 
      image[IMAGE[id[x]], OMEGA]

application: reify rules

In this final section the result of the preceding section is used to derive a reify rule for partenum and for enum.

Lemma.  A simplification rule.

equal[intersection[partenum[x], ENUMS], partenum[x]]

intersection[ENUMS, partenum[x_]] := partenum[x]

Lemma.  A simplification rule.

SubstTest[composite, funpart[t], inverse[funpart[t]], 
        t -> composite[id[ENUMS], inverse[IMAGE[SECOND]]]] // 
      Reverse

composite[id[ENUMS], inverse[IMAGE[SECOND]], IMAGE[SECOND], id[ENUMS]] := 
      id[ENUMS]

Theorem.  A formula for partenum[x].

ImageComp[composite[id[ENUMS], inverse[IMAGE[SECOND]]], 
        composite[IMAGE[SECOND], id[ENUMS]], partenum[x]] // 
      Reverse

intersection[ENUMS, 
        image[inverse[IMAGE[SECOND]], image[IMAGE[id[x_]], OMEGA]]] := 
      partenum[x]

Theorem.   A reify rule for partenum.

SubstTest[reify, x, 
        intersection[t, 
          image[inverse[IMAGE[SECOND]], image[IMAGE[id[f[x]]], OMEGA]]], 
        t -> ENUMS] // Reverse

reify[x_, partenum[y_]] := 
      composite[id[ENUMS], inverse[IMAGE[SECOND]], IMAGE[SECOND], 
        IMAGE[id[reify[x, y]]], CART, id[cart[V, OMEGA]], inverse[FIRST], 
        SINGLETON]

Corollary.  A reify rule for enum.

SubstTest[reify, x, image[t, partenum[f[x]]], t -> inverse[E]] // 
      Reverse

reify[x_, enum[y_]] := 
      composite[inverse[E], id[ENUMS], inverse[IMAGE[SECOND]], IMAGE[SECOND], 
        IMAGE[id[reify[x, y]]], CART, id[cart[V, OMEGA]], inverse[FIRST], 
        SINGLETON]