Veblen’s theorem illustrated

Johan G. F. Belinfante
2011 July 31

SetDirectory["l:"];  << goedel.11jul31a

summary

A special case of a theorem due to Veblen is derived using the compound wrapper pco[Uclosed[x]] for a Uclosed proper class of ordinals.

"Oswald Veblen, Continuous increasing functions of finite and transfinite ordinals, Transactions of the American Mathematical Society, volume 9 (no. 3), pp. 280-292.";

As an example, it is shown that there is no ordinal can be an upper bound for the fixed points of the function enum[fix[CARD]] that enumerates all cardinals in strictly increasing order.

temporary abbreviations

The following temporary abbreviations will help to save some writing.  When there is no chance of confusion, the variables  x  and  y  will be suppressed in the informal comments accompanying the derivations.  Thus, for example,  f[x]  will be further abbreviated to  f.

f[x_] := enum[pco[Uclosure[x]]]

For any given ordinal  ord[y], the list it[x, y]  =  iterate[f[x], {ord[y]}]  of iterates obtained by applying  f[x]  repeatedly is a monotone function.

it[x_, y_] := iterate[enum[pco[Uclosure[x]]], set[ord[y]]]

The range of it[x, y] is a hull expression that will be abbreviated as  h[x, y].  This is a subclass of  Ω.

h[x_, y_] := 
      hull[invar[enum[pco[Uclosure[x]]]], set[ord[y]]]

The goal will be to show that U[h[x, y]] ∈ Ω  is a fixed point of  f[x].

The idea is to use reductio ad absurdum.  The hypothetical statement that there are no fixed points of  f[x]  at or above ord[y]  will be abbreviated as hyp[x, y].

hyp[x_, y_] := 
      not[member[ord[y], 
          image[inverse[S], fix[enum[pco[Uclosure[x]]]]]]]

The strategy of the derivation to be presented below can be briefly summarized as follows.  If  x ∈  U[h] = U[range[it]] then there exists an ordinal  y ∈ h = range[it]  with  x ∈ y.  That is, there exists a natural number  z  such that  y = it(z).  Then  f(x) ∈ f(y) = f(it(z)) = it(succ[z]) ⊂ U[h], which implies  f(x) ∈  U[h].  Since x ∈ U[h] implies f(x) ∈ U[h], it follows that U[h] is invariant under f.   That is:  image[f, U[h]] ⊂ U[h].  The sum classes therefore satisfy  f(U[h]) = U[image[f, U[h]]] ⊂ U[U[h]] =U[h].  Finally, since it is known that  U[h] ⊂ f(U[h]), one can conclude that  f(U[h]) = U[h].

derivation

Theorem.   The iteration goes on forever.  That is, the list of iterates is infinitely long.

SubstTest[implies, 
        and[member[v, domain[funpart[u]]], 
          invariant[funpart[u], domain[funpart[u]]]], 
        equal[omega, 
          domain[iterate[funpart[u], set[v]]]], {u -> enum[pco[x]], 
          v -> ord[y]}] // Reverse

domain[iterate[enum[pco[x_]], set[ord[y_]]]] := omega

Lemma.     The ordinal it(z)  appearing on the list of  it  at any point z ∈ ω  belongs to  h.

Map[
        implies[equal[omega, 
              domain[iterate[enum[pco[x]], set[ord[y]]]]], #] &, 
        SubstTest[member, APPLY[funpart[t], nat[z]], range[funpart[t]], 
          t -> iterate[enum[pco[x]], set[ord[y]]]]] // 
      Reverse

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

Corollary.   it(z) ⊂ U[h].

SubstTest[implies, member[u, v], 
        subclass[u, 
          U[v]], {u -> APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          v -> hull[invar[enum[pco[x]]], set[ord[y]]]}] // Reverse

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

Theorem.    y ⊂ U[h].

SubstTest[subclass, APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
        U[hull[invar[enum[pco[x]]], set[ord[y]]]], z -> 0] // 
      Reverse

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

Corollary.

equal[
      intersection[ord[y], 
        complement[U[hull[invar[enum[pco[x]]], set[ord[y]]]]]], 0]

intersection[complement[U[hull[invar[enum[pco[x_]]], set[ord[y_]]]]], 
        ord[y_]] := 0

Theorem.       it(z) ∈ Ω

SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, 
          w], {u -> APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          v -> hull[invar[enum[pco[x]]], set[ord[y]]], w -> OMEGA}] // 
      Reverse

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

Lemma.  Monotone property of  it.

SubstTest[implies, 
        and[member[u, domain[t]], subclass[P[t], monotone[S, S]], 
          subclass[u, v]], subclass[APPLY[t, u], APPLY[t, v]], 
        t -> iterate[enum[pco[x]], set[ord[y]]]] // Reverse

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

Theorem.

Map[not, 
      SubstTest[subclass, ord[y], ord[t], 
        t -> APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]]]

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

Theorem.

SubstTest[or, member[ord[u], image[inverse[S], fix[enum[pco[x]]]]], 
        member[ord[v], ord[u]], 
        not[member[ord[v], fix[enum[pco[x]]]]], {u -> y, 
          v -> APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]}] // 
      Reverse

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

Lemma.

SubstTest[implies, 
        and[equal[APPLY[funpart[t], u], u], member[u, domain[funpart[t]]]], 
        member[u, 
          fix[funpart[t]]], {u -> 
            APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          t -> enum[pco[x]]}] // Reverse

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

Theorem.   it(z)  is not a fixed point of  f.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> 
              not[member[ord[y], image[inverse[S], fix[enum[pco[x]]]]]], 
            p2 -> 
              not[member[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
                  fix[enum[pco[x]]]]], 
            p3 -> 
              not[equal[
                  APPLY[enum[pco[x]], 
                    APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]], 
                  APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]]]}]] // 
      Reverse

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

Theorem.      f(it(z)) ⊂ U[h].

SubstTest[subclass, APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[t]], 
        U[hull[invar[enum[pco[x]]], set[ord[y]]]], t -> succ[nat[z]]] // 
      Reverse

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

Corollary.

Map[not, 
      SubstTest[subclass, ord[u], 
        ord[v], {u -> 
            APPLY[enum[pco[x]], 
              APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]], 
          v -> U[hull[invar[enum[pco[x]]], set[ord[y]]]]}]]

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

Theorem   Strict monotonicity.    it(z) ∈ f(it(z)).

Map[
      implies[not[
            member[ord[y], image[inverse[S], fix[enum[pco[x]]]]]], #] &, 
      SubstTest[and, subclass[ord[u], ord[v]], 
        not[equal[ord[u], ord[v]]], {u -> 
            APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          v -> 
            APPLY[iterate[enum[pco[x]], set[ord[y]]], 
              succ[nat[z]]]}]]

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

Theorem.   it(z) ∈ U[h].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> 
              not[member[ord[y], image[inverse[S], fix[enum[pco[x]]]]]], 
            p2 -> member[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
                APPLY[enum[pco[x]], 
                  APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]]], 
            p3 -> member[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
                U[hull[invar[enum[pco[x]]], set[ord[y]]]]]}]] // 
      Reverse

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

Corollary.    y ∈ U[h].

SubstTest[or, 
        member[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          U[hull[invar[enum[pco[x]]], set[ord[y]]]]], 
        member[ord[y], image[inverse[S], fix[enum[pco[x]]]]], z -> 0] // 
      Reverse

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

Eliminating the variable  z  yields   h ⊂ U[h].

Theorem.    hyp ⟹  h ⊂ U[h].

Map[empty, 
      SubstTest[reify, z, 
        intersection[
          complement[
            image[V, 
              intersection[fix[enum[pco[x]]], image[S, set[ord[y]]]]]], 
          dif[set[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]], t]], 
        t -> U[hull[invar[enum[pco[x]]], set[ord[y]]]]]]

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

Lemma.

SubstTest[implies, and[subclass[t, OMEGA], subclass[t, U[t]]], 
        equal[U[U[t]], U[t]], t -> hull[invar[enum[pco[x]]], set[ord[y]]]] // 
      Reverse

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

Theorem.   hyp  ⟹  UU[h]] = U[h].   (That is,  U[h]  is a limit ordinal.)

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> 
              not[member[ord[y], image[inverse[S], fix[enum[pco[x]]]]]], 
            p2 -> subclass[hull[invar[enum[pco[x]]], set[ord[y]]], 
                U[hull[invar[enum[pco[x]]], set[ord[y]]]]], 
            p3 -> equal[U[hull[invar[enum[pco[x]]], set[ord[y]]]], 
                U[U[hull[invar[enum[pco[x]]], set[ord[y]]]]]]}]] // 
      Reverse

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

The Uclosedness hypothesis is needed here:

Theorem.   A continuity property of the enumerator of  pco[Uclosure[x]].

SubstTest[implies, subclass[ord[y], domain[enum[Uclosure[t]]]], 
        equal[APPLY[enum[Uclosure[t]], U[ord[y]]], 
          U[image[enum[Uclosure[t]], ord[y]]]], t -> pco[Uclosure[x]]] // 
      Reverse

U[image[enum[pco[Uclosure[x_]]], ord[y_]]] := 
      APPLY[enum[pco[Uclosure[x]]], U[ord[y]]]

Theorem.

SubstTest[U, image[enum[pco[Uclosure[x]]], ord[z]], 
        z -> U[hull[invar[enum[pco[Uclosure[x]]]], set[ord[y]]]]] // 
      Reverse

U[image[enum[pco[Uclosure[x_]]], 
          U[hull[invar[enum[pco[Uclosure[x_]]]], set[ord[y_]]]]]] := 
      APPLY[enum[pco[Uclosure[x]]], 
        U[U[hull[invar[enum[pco[Uclosure[x]]]], set[ord[y]]]]]]

executing the strategy

Lemma.

SubstTest[implies, and[member[u, v], member[v, OMEGA]], 
        member[u, OMEGA], 
        v -> APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]] // 
      Reverse

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

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          implies[p3, p4], 
          not[implies[p1, p4]], {p1 -> 
              member[t, APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]], 
            p2 -> member[t, OMEGA], 
            p3 -> 
              member[APPLY[enum[pco[x]], t], 
                APPLY[enum[pco[x]], 
                  APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]]]], 
            p4 -> 
              member[APPLY[enum[pco[x]], t], 
                U[hull[invar[enum[pco[x]]], set[ord[y]]]]]}]] // 
      Reverse

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

Theorem.   (Eliminate  t.)

Map[equal[V, #] &, 
      SubstTest[class, t, 
        implies[member[t, u], 
          member[APPLY[funpart[w], t], v]], {u -> 
            APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], 
          v -> U[hull[invar[enum[pco[x]]], set[ord[y]]]], 
          w -> enum[pco[x]]}]]

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

Theorem.   (Eliminate  z.)

Map[
        implies[empty[range[complement[#]]], 
            invariant[enum[pco[x]], 
              U[hull[invar[enum[pco[x]]], set[ord[y]]]]]] &, 
        SubstTest[reify, z, 
          complement[
            dif[APPLY[iterate[enum[pco[x]], set[ord[y]]], nat[z]], t]], 
          t -> 
            image[inverse[enum[pco[x]]], 
              U[hull[invar[enum[pco[x]]], set[ord[y]]]]]]] // 
      Reverse

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

Lemma.

Map[
      implies[subclass[
            APPLY[enum[pco[x]], U[hull[invar[enum[pco[x]]], set[ord[y]]]]], 
            U[hull[invar[enum[pco[x]]], set[ord[y]]]]], #] &, 
      SubstTest[and, subclass[u, v], 
        subclass[v, 
          u], {u -> 
            APPLY[enum[pco[x]], U[hull[invar[enum[pco[x]]], set[ord[y]]]]], 
          v -> U[hull[invar[enum[pco[x]]], set[ord[y]]]]}]]

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

Lemma.

SubstTest[implies, subclass[u, v], 
        subclass[U[u], U[v]], {u -> image[f[x], U[h[x, y]]], 
          v -> U[h[x, y]]}] // Reverse

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

Theorem.    hyp  ⟹  f(U[h]) = U[h].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], implies[p3, p4], 
          not[implies[p1, p4]], {p1 -> hyp[x, y], 
            p2 -> equal[U[U[h[x, y]]], U[h[x, y]]], 
            p3 -> subclass[APPLY[f[x], U[h[x, y]]], U[h[x, y]]], 
            p4 -> equal[APPLY[f[x], U[h[x, y]]], U[h[x, y]]]}]] // 
      Reverse

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

Corollary.

SubstTest[implies, and[equal[APPLY[funpart[u], v], v], member[v, w]], 
        member[v, fix[funpart[u]]], {u -> f[x], v -> U[h[x, y]], 
          w -> V}] // Reverse

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

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> hyp[x, y], 
            p2 -> equal[APPLY[f[x], U[h[x, y]]], U[h[x, y]]], 
            p3 -> member[U[h[x, y]], fix[f[x]]]}]] // Reverse

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

Theorem.

SubstTest[implies, and[subclass[u, v], member[v, w]], 
        member[u, image[inverse[S], w]], {u -> ord[y], 
          v -> U[h[x, y]], w -> fix[f[x]]}] // Reverse

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

Theorem.

SubstTest[and, implies[p, q], 
      or[p, q], {p -> member[U[h[x, y]], fix[f[x]]], 
        q -> not[hyp[x, y]]}]

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

Theorem.  Eliminate  y.   (This inclusion can be improved upon.)

Map[or[subclass[OMEGA, image[inverse[S], fix[f[x]]]], empty[#]] &, 
      SubstTest[reify, y, dif[set[ord[y]], t], 
        t -> image[inverse[S], fix[f[x]]]]]

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

Corollary.

SubstTest[or, equal[OMEGA, U[t]], 
        not[subclass[OMEGA, image[inverse[S], t]]], not[subclass[t, OMEGA]], 
        t -> fix[f[x]]] // Reverse

U[fix[enum[pco[Uclosure[x_]]]]] := OMEGA

Corollary.  (Improvement of the lemma above.)

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> image[inverse[S], fix[enum[pco[Uclosure[x]]]]], 
        v -> P[OMEGA]}]

image[inverse[S], fix[enum[pco[Uclosure[x_]]]]] := P[OMEGA]

The final step is to eliminate the double wrapper pco[Uclosure[x]].

Veblen’s Theorem.   If  x  is a proper Uclosed class of ordinals, then  U[fix[enum[x]]] = Ω.

SubstTest[implies, equal[x, pco[Uclosure[t]]], 
        equal[OMEGA, U[fix[enum[x]]]], t -> x] // Reverse

or[equal[OMEGA, U[fix[enum[x_]]]], member[x_, V], 
        not[equal[x_, Uclosure[x_]]], not[subclass[x_, OMEGA]]] := 
      True

The following provides an example.

Corollary.  Every ordinal is less than some fixed point of  enum[fix[CARD]].

SubstTest[or, equal[OMEGA, U[fix[enum[x]]]], member[x, V], 
        not[equal[x, Uclosure[x]]], not[subclass[x, OMEGA]], 
        x -> fix[CARD]] // Reverse

U[fix[enum[fix[CARD]]]] := OMEGA