SMALLER for wellorderable sets

Johan G. F. Belinfante
2007 May 3

SetDirectory["l:"]; << goedel93.03a; << tools.m

summary

A set x is wellorderable if it is equipollent to some ordinal number. For each such set x, the smallest ordinal equipollent to x is its cardinality card[x].  If  x is not wellorderable, then card[x] = V.  The function CARD assigns to each wellorderable set its cardinality.  The domain of this function is the class image[Q,OMEGA] of wellorderable sets.

domain[CARD]

A wrapper wob[x] for wellorderable sets has been introduced.  Wellorderable sets are equipollent if they have the same cardinality:

member[pair[wob[x], wob[y]], Q]

A set x is smaller than a set y if x is equipollent to a subset of y, but not to y itself.  The corresponding relation is:

class[pair[x, y], 
      and[not[member[pair[x, y], Q]], 
        exists[z, and[subclass[z, y], member[pair[x, z], Q]]]]]

In this notebook it is shown that a wellorderable set is smaller than another if and only if it has a lesser cardinality.

a membership rule

member[pair[x, y], composite[inverse[CARD], z]] // 
      AssertTest

member[pair[x_, y_], composite[inverse[CARD], z_]] := 
      and[member[x, V], member[y, image[Q, OMEGA]], 
        member[pair[x, card[y]], z]]

facts about SMALLER

Lemma.  (Simpification rule.)

equiv[and[member[x, V], member[pair[x, y], SMALLER]], 
      member[pair[x, y], SMALLER]]

and[member[x_, V], member[pair[x_, y_], SMALLER]] := 
      member[pair[x, y], SMALLER]

Theorem.  A set cannot be smaller than any of its subsets.

SubstTest[implies, and[member[u, v], subclass[v, w]], 
          member[u, w], 
{u -> pair[x, y], 
            v -> SMALLER, w -> complement[inverse[S]]}] // 
        Reverse // MapNotNot

or[not[member[pair[x_, y_], SMALLER]], not[subclass[y_, x_]]] := 
      True

Corollary.  No set can be smaller than itself.

Map[not, 
      SubstTest[implies, member[pair[x, y], SMALLER], not[subclass[y, x]], 
          y -> x] // Reverse]

member[pair[x_, x_], SMALLER] := False

smaller sets

Theorem.

SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, w], 
{u -> pair[x, y], 
          v -> composite[inverse[CARD], E, CARD], w -> SMALLER}] // 
      Reverse

or[member[pair[x_, y_], SMALLER], not[member[y_, image[Q, OMEGA]]], 
        not[member[card[x_], card[y_]]]] := True

Corollary.  (Replacing the wellorderable literal with a wob wrapper.)

SubstTest[or, member[pair[x, t], SMALLER], 
        not[member[t, image[Q, OMEGA]]], not[member[card[x], card[t]]], 
        t -> wob[y]] // Reverse

or[member[pair[x_, wob[y_]], SMALLER], 
        not[member[card[x_], card[wob[y_]]]]] := True

Theorem.

Map[not, 
      SubstTest[member, pair[wob[x], wob[y]], 
        intersection[u, v], {u -> Q, v -> SMALLER}]]

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

Lemma.

Map[not, 
      SubstTest[member, pair[wob[x], wob[y]], 
        intersection[u, v], 
{u -> SMALLER, 
          v -> composite[inverse[CARD], inverse[S], CARD]}]]

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

Main Theorem.

equiv[member[pair[wob[x], wob[y]], SMALLER], 
      member[card[wob[x]], card[wob[y]]]]

member[pair[wob[x_], wob[y_]], SMALLER] := 
      member[card[wob[x]], card[wob[y]]]

a variable-free formulation

Eliminating the wob wrappers yields:

SubstTest[implies, 
        and[equal[x, wob[u]], equal[y, wob[v]], member[pair[x, y], SMALLER]], 
        member[card[x], card[y]], {u -> x, v -> y}] // 
      Reverse

or[member[card[x_], card[y_]], not[member[pair[x_, y_], SMALLER]], 
        not[member[x_, image[Q, OMEGA]]], not[member[y_, image[Q, OMEGA]]]] := 
      True

Lemma.

SubstTest[empty, 
      dif[u, v], {u -> 
          composite[id[image[Q, OMEGA]], SMALLER, id[image[Q, OMEGA]]], 
        v -> composite[inverse[CARD], E, CARD]}]

% /. Equal -> SetDelayed

Theorem.  A formula for the restriction of SMALLER to wellorderable sets.

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> composite[id[image[Q, OMEGA]], SMALLER, 
            id[image[Q, OMEGA]]], 
        v -> composite[inverse[CARD], E, CARD]}]

composite[id[image[Q, OMEGA]], SMALLER, id[image[Q, OMEGA]]] := 
      composite[inverse[CARD], E, CARD]