cardinalities of subsets of a finite set

Johan G. F. Belinfante
2005 November 4

SetDirectory["l:"];  << goedel75.02a; << tools.m

summary

If  x  is a finite set, then the cardinality of its subsets cannot exceed that of  x  itself, and there exist subsets of each possible size.  To prove these facts, the special case that  x  is a natural number is considered first, anf then the result is generalized to an arbitrary finite set using the equipollence relation  Q.

some basic results about cardinality

Since subclass for card now gets rewritten in terms of member, some new rewrite rules are needed to cope with the properties of subclass.  For example, the reflexive property of subclass now becomes a statement about negated self-membership.

Map[not, SubstTest[subclass, card[x], card[y], y -> x]] // 
      Reverse

member[card[x_], card[x_]] := False

Theorem.  The fullness of card[x] is not automatically rewritten, but it has this consequence:

Map[not, 
      SubstTest[implies, and[member[u, v], subclass[v, u]], 
        member[u, u], {u -> card[x], v -> U[card[x]]}]]

member[card[x_], U[card[x_]]] := False

Corollary.  (a law of dichotomy)

SubstTest[implies, and[member[u, v], member[v, u]], 
      member[u, U[u]], 
{u -> card[x], 
        v -> card[y]}]

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

Equality rule:  (antisymmetry of subclass)

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> card[x], v -> card[y]}]

and[not[member[card[x_], card[y_]]], not[member[card[y_], card[x_]]]] := 
      equal[card[x], card[y]]

upper bound

The cardinality of a disjoint union of finite sets is the sum of their cardinalities.  The special case that one of these sets is a natural number is considered here.

SubstTest[implies, 
      and[member[u, FINITE], member[v, FINITE], disjoint[u, v]], 
      equal[natadd[card[u], card[v]], card[union[u, v]]], {u -> fin[x], 
        v -> dif[nat[y], fin[x]]}]

natadd[card[fin[x_]], 
        card[intersection[complement[fin[x_]], nat[y_]]]] := 
      card[union[fin[x], nat[y]]]

The sum of two numbers cannot be less than either one.  This observation yields the following corollary of the preceding equation.  Note that natadd has now been eliminated.

Map[not, 
      SubstTest[subclass, u, 
        natadd[u, v], {u -> card[fin[x]], 
          v -> card[intersection[dif[nat[y], fin[x]]]]}]]

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

Remove the fin wrappers.

SubstTest[implies, and[equal[x, fin[u]]], 
      not[member[card[union[x, nat[y]]], card[x]]], u -> x]

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

The following trick eliminates union in favor of subclass.

SubstTest[implies, and[member[x, FINITE], equal[z, union[x, nat[y]]]], 
      not[member[card[z], card[x]]], z -> nat[y]]

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

This can be cleaned up, renoving the finiteness hypothesis.   This says that a natural number can not be less than the cardinality of one of its subsets.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        not[implies[p1, p3]], {p1 -> subclass[x, nat[y]], 
          p2 -> member[x, FINITE], 
          p3 -> not[member[nat[y], card[x]]]}]]

or[not[member[nat[y_], card[x_]]], not[subclass[x_, nat[y_]]]] := 
      True

removing the variables

Lemma. (dichotomy)

SubstTest[subclass, card[x], card[z], z -> nat[y]]

subclass[card[x_], nat[y_]] := not[member[nat[y], card[x]]]

Lemma.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], {p1 -> subclass[x, nat[y]], 
          p2 -> member[x, FINITE], 
          p3 -> member[x, image[Q, OMEGA]]}]]

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

Lemma to prepare for eliminating the variable  x.

implies[member[x, P[nat[y]]], 
        member[x, image[inverse[CARD], P[nat[y]]]]] // NotNotTest

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

Map[equal[V, #] &, 
        SubstTest[class, w, 
          implies[member[w, P[u]], member[w, v]], {u -> nat[x], 
            v -> image[inverse[CARD], P[nat[x]]]}]] // Reverse

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

Corollary.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], {u -> P[nat[x]], 
        v -> FINITE, w -> CARD}]

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

Lemma.

equal[intersection[omega, image[CARD, P[nat[x]]]], 
      image[CARD, P[nat[x]]]]

intersection[omega, image[CARD, P[nat[x_]]]] := 
      image[CARD, P[nat[x]]]

Theorem:  The set of cadinalities of the subsets of a natural number is contained in its successor.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> P[nat[x]], 
        v -> image[inverse[CARD], P[card[nat[x]]]], 
        w -> composite[id[omega], CARD]}]

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

lower bound for the nat case

Any natural number is its own cardinality.    The number  x  itself is a subset with cardinality  x.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], {u -> set[nat[x]], 
        v -> P[nat[x]], w -> CARD}]

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

The members of a natural number provide instances of subsets with all possible smaller cardinalities.

ImageComp[CARD, id[omega], nat[x]] // Reverse

image[CARD, nat[x_]] := nat[x]

Corollary.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], {u -> nat[x], 
        v -> P[nat[x]], w -> CARD}]

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

These results can be combined with the inclusion derived in the preceding section to obtain an equation:

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> image[CARD, P[nat[x]]], 
        v -> succ[nat[x]]}]

image[CARD, P[nat[x_]]] := succ[nat[x]]

The variable x  can now be removed:

Map[composite[#, id[omega]] &, 
        SubstTest[reify, x, image[CARD, P[f[x]]], f -> nat]] // 
      Reverse

composite[CARD, inverse[S], id[omega]] := 
      composite[id[omega], inverse[S], id[omega]]

general case

The general case of an arbitrary finite set is obtained as a corollary in this section, using the equipollence relation Q.  One lemma is needed.

Assoc[composite[CARD, inverse[S]], Q, id[omega]]

composite[CARD, inverse[S], inverse[CARD], id[omega]] := 
      composite[id[omega], inverse[S], id[omega]]

The main theorem is first derived in variable-free form:

Assoc[composite[CARD, inverse[S]], Q, id[FINITE]] // Reverse

composite[CARD, inverse[S], id[FINITE]] := 
      composite[id[omega], inverse[S], id[omega], CARD]

This result becomes more easily understood if variables are reintroduced:

ImageComp[CARD, composite[inverse[S], id[FINITE]], set[fin[x]]] // 
      Reverse

image[CARD, P[fin[x_]]] := succ[card[fin[x]]]

SubstTest[implies, 
      and[member[pair[u, v], composite[Id, w]], member[u, z]], 
      member[v, image[w, z]], {u -> x, v -> card[x], 
        w -> CARD, z -> P[fin[y]]}]

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

Theorem.  The cardinality of a finite set cannot be smaller than that of one of its subsets.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        implies[and[p1, p3], or[p4, p5]], implies[p4, p6], implies[p5, p6], 
        not[implies[p1, p6]], {p1 -> subclass[x, fin[y]], 
          p2 -> member[x, FINITE], 
          p3 -> member[x, image[Q, OMEGA]], 
p4 -> 
            equal[card[x], card[fin[y]]], 
          p5 -> member[card[x], card[fin[y]]], 
          p6 -> not[member[card[fin[y]], card[x]]]}]]

or[not[member[card[fin[y_]], card[x_]]], not[subclass[x_, fin[y_]]]] := 
      True