an explicit formula for LUB[id[ω] ∘ S ∘ id[ω]]

Johan G. F. Belinfante
2010 September 19

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

summary

In this notebook is shown that the LUB function for the restriction id[ω] ∘ S ∘ id[ω]  of the subset relation  S  to the set  ω  of natural numbers is equal to the restriction of the function BIGCUP to the set image[inverse[S], ω] of finite subsets of ω.   The basic idea of the derivation is that two functions are equal if one is a subclass of the other, and their domains are equal.   The fact that the relation id[ω] ∘ S ∘ id[ω]  is conditionally complete is used to obtain a formula for the domain of its LUB function.

the domain of the LUB function

In this section a temporary rule for the domain of the LUB function is derived.

Lemma.  A simplification rule.

equal[
        intersection[image[inverse[BIGCUP], image[inverse[S], omega]], 
          P[omega]], image[inverse[S], omega]] // AssertTest

intersection[image[inverse[BIGCUP], image[inverse[S], omega]], 
        P[omega]] := image[inverse[S], omega]

Since  id[ω] ∘ S ∘ id[ω]  is a well ordering, it is conditionally complete.    A lower bound on the domain of LUB is obtained using this fact.   (Here CC is the class of all conditionally complete relations.)

Theorem.  A lower bound on the domain of LUB.

SubstTest[implies, member[x, CC], 
        subclass[domain[UB[x]], union[set[0], domain[LUB[x]]]], 
        x -> restrict[S, omega, omega]] // Reverse

% /. Equal -> SetDelayed

Not every subset of ω has an upper bound, let alone a least upper bound.

Theorem.  An upper bound on the domain of LUB.

SubstTest[subclass, domain[LUB[x]], domain[UB[x]], 
        x -> composite[id[omega], S, id[omega]]] // Reverse

% /. Equal -> SetDelayed

Theorem.  An explicit formula for the domain of LUB.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> image[inverse[S], omega], 
        v -> domain[LUB[composite[id[omega], S, id[omega]]]]}]

domain[LUB[composite[id[omega], S, id[omega]]]] := 
      image[inverse[S], omega]

an explicit formula for the LUB function

The expression  ω ⋂ fin[t] serves as a compound wrapper for a finite set of natural numbers.

Lemma.

equal[intersection[omega, U[intersection[omega, x]]], 
      U[intersection[omega, x]]]

intersection[omega, U[intersection[omega, x_]]] := 
      U[intersection[omega, x]]

Lemma.

Map[not, 
        SubstTest[implies, member[t, image[inverse[S], omega]], 
          not[equal[U[t], omega]], t -> intersection[fin[x], omega]]] // 
      Reverse

equal[omega, U[intersection[omega, fin[x_]]]] := False

Lemma.    A special case of a theorem about ordinals.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> subclass[x, omega], 
            p2 -> subclass[x, OMEGA], p3 -> subclass[x, succ[U[x]]]}]] // 
      Reverse

or[not[subclass[x_, omega]], subclass[x_, succ[U[x_]]]] := 
      True

Corollary.  A wrapper version of the preceding theorem.

SubstTest[implies, subclass[t, omega], subclass[t, succ[U[t]]], 
        t -> intersection[x, omega]] // Reverse

subclass[intersection[omega, x_], succ[U[intersection[omega, x_]]]] := 
      True

Lemma.

SubstTest[implies, member[t, REGULAR], 
        member[intersection[t, x], REGULAR], t -> omega] // 
      Reverse

member[intersection[omega, x_], REGULAR] := True

Lemma.  A consequence of regularity.

SubstTest[member, reg[t], image[inverse[S], reg[t]], 
        t -> U[intersection[omega, x]]] // Reverse

member[U[intersection[omega, x_]], 
        image[inverse[S], U[intersection[omega, x_]]]] := False

Lemma.

(SubstTest[implies, and[member[x, V], member[y, lub[z, x]]], 
            member[pair[x, y], LUB[z]], {y -> U[x], 
              z -> restrict[S, omega, omega]}] /. 
          x -> intersection[omega, fin[t]]) // Reverse

(% /. t -> t_) /. Equal -> SetDelayed

Lemma.  Removal of the compound wrapper  ω ⋂ fin[t].

SubstTest[implies, equal[x, intersection[omega, fin[t]]], 
        member[pair[x, U[x]], LUB[composite[id[omega], S, id[omega]]]], 
        t -> x] // Reverse

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

Lemma.     Eliminating variables.

Map[composite[Id, complement[#]] &, 
      SubstTest[class, pair[x, y], 
        implies[member[pair[x, y], u], 
          member[pair[x, y], v]], {u -> 
            composite[BIGCUP, id[image[inverse[S], omega]]], 
          v -> LUB[composite[id[omega], S, id[omega]]]}]]

% /. Equal -> SetDelayed

Lemma.  An inclusion.

SubstTest[empty, 
      dif[u, v], {u -> composite[BIGCUP, id[image[inverse[S], omega]]], 
        v -> LUB[composite[id[omega], S, id[omega]]]}]

% /. Equal -> SetDelayed

Main Theorem.  An explicit formula for the LUB function of the relation id[ω] ∘ S ∘ id[ω].

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
        equal[u, 
          composite[v, id[domain[u]]]], {u -> 
            composite[BIGCUP, id[image[inverse[S], omega]]], 
          v -> LUB[composite[id[omega], S, id[omega]]]}] // 
      Reverse

LUB[composite[id[omega], S, id[omega]]] := 
      composite[BIGCUP, id[image[inverse[S], omega]]]