ZN restricted to OMEGA

Johan G. F. Belinfante
2006 March 14

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

introduction

Statements about the Zermelo-von Neumann cumulative hierarchy are formulated in the GOEDEL program in terms of the relation  ZN  which is the largest relation that commutes with the inverse membership relation.

commute[ZN, inverse[E]]

implies[subcommute[x, E], subclass[inverse[x], ZN]]

When the relation  ZN  is restricted to the class OMEGA of ordinal numbers, it is rewritten in terms of the inverse of the rank function  RANK.

composite[ZN, id[OMEGA]]

In this notebook some basic rewrite rules are derived that help in translating results about ZN involving ordinals to statements involving rank.

thinpart[ZN]

Some rewrite rules yield expressions involving thinpart[ZN].  When one restricts to the class REGULAR, the relation thinpart[ZN] is the same as ZN.

Assoc[ZN, id[domain[VERTSECT[ZN]]], id[REGULAR]] // Reverse

composite[thinpart[ZN], id[REGULAR]] := 
      composite[ZN, id[REGULAR]]

In particular, one can remove the thinpart wrapper for restrictions to OMEGA.

Assoc[thinpart[ZN], id[REGULAR], id[OMEGA]]

composite[thinpart[ZN], id[OMEGA]] := 
      composite[inverse[RANK], inverse[S], id[OMEGA]]

image rules

Lemma.

IminComp[id[OMEGA], RANK, image[inverse[S], ord[x]]]

image[inverse[RANK], image[inverse[S], ord[x_]]] := 
      image[inverse[RANK], ord[x]]

Theorem.

ImageComp[ZN, id[OMEGA], ord[x]] // Reverse

image[ZN, ord[x_]] := image[inverse[RANK], ord[x]]

Corollary.

ImageComp[ZN, id[OMEGA], set[ord[x]]]

image[inverse[RANK], P[ord[x_]]] := 
      P[image[inverse[RANK], ord[x]]]

reify results

The results of the preceding section can be formulated without variables.  Using reify, one finds:

Map[composite[VERTSECT[#], id[OMEGA]] &, 
        SubstTest[reify, x, image[inverse[RANK], image[inverse[S], f[x]]], 
          f -> ord]] // Reverse

composite[IMAGE[inverse[RANK]], IMAGE[inverse[S]], id[OMEGA]] := 
      composite[IMAGE[inverse[RANK]], id[OMEGA]]

Similarly,

Map[composite[VERTSECT[#], id[OMEGA]] &, 
        SubstTest[reify, x, image[ZN, f[x]], f -> ord]] // 
      Reverse

composite[IMAGE[ZN], id[OMEGA]] := 
      composite[IMAGE[inverse[RANK]], id[OMEGA]]

Corollary.

Assoc[POWER, IMAGE[ZN], id[OMEGA]] // Reverse

composite[VERTSECT[ZN], id[OMEGA]] := 
      composite[POWER, IMAGE[inverse[RANK]], id[OMEGA]]

membership rule

Lemma.

member[pair[u, v], composite[inverse[RANK], w]] // 
      AssertTest

member[pair[u_, v_], composite[inverse[RANK], w_]] := 
      and[member[u, V], member[v, REGULAR], 
        member[pair[u, rank[v]], w]]

Lemma.

SubstTest[implies, and[subclass[u, v], member[v, V]], 
      member[u, V], {u -> rank[x], v -> ord[y]}]

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

equiv[and[member[x, REGULAR], subclass[rank[x], ord[y]]], 
      subclass[rank[x], ord[y]]]

and[member[x_, REGULAR], subclass[rank[x_], ord[y_]]] := 
      subclass[rank[x], ord[y]]

Corollary.

SubstTest[and, member[x, V], 
      and[member[x, REGULAR], subclass[rank[x], z]], 
      z -> ord[y]]

and[member[x_, V], subclass[rank[x_], ord[y_]]] := 
      subclass[rank[x], ord[y]]

The following rewrite rule is the main result of this section.

SubstTest[member, pair[u, y], 
        composite[z, id[OMEGA]], {u -> ord[x], z -> ZN}] // 
      Reverse

member[pair[ord[x_], y_], ZN] := subclass[rank[y], ord[x]]

A similar result holds for thinpart[ZN].

SubstTest[member, pair[ord[x], y], composite[z, id[OMEGA]], 
        z -> thinpart[ZN]] // Reverse

member[pair[ord[x_], y_], thinpart[ZN]] := 
      subclass[rank[y], ord[x]]

subclass rule

Lemma.

SubstTest[implies, and[subclass[x, z], member[z, V]], member[x, V], 
      z -> image[ZN, ord[y]]]

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

equiv[and[member[x, V], subclass[x, image[inverse[RANK], ord[y]]]], 
      subclass[x, image[inverse[RANK], ord[y]]]]

and[member[x_, V], subclass[x_, image[inverse[RANK], ord[y_]]]] := 
      subclass[x, image[inverse[RANK], ord[y]]]

Corollary.

SubstTest[member, pair[ord[y], x], composite[inverse[E], w], 
        w -> VERTSECT[ZN]] // Reverse

subclass[x_, image[inverse[RANK], ord[y_]]] := 
      subclass[rank[x], ord[y]]