NATEXP, part 4.

Johan G. F. Belinfante
2006 July 2

SetDirectory["l:"]; << goedel83.01a; << tools.m

summary

In this fourth notebook in a series about exponentiation for natural numbers it is shown by induction that the number of subsets of a natural number  n  is  (2^n).  More generally, the cardinality of the power set of any finite set x is equal to (2^(card[x])).

ADJOIN

The restriction of ADJOIN[set[x]] to the power set of a natural number x is one-to-one.

Map[subclass[intersection[#, cart[P[nat[x]], P[nat[x]]]], Id] &, 
      composite[inverse[ADJOIN[set[nat[x]]]], ADJOIN[set[nat[x]]]] // 
        RelnNormality]

FUNCTION[composite[id[P[nat[x_]]], inverse[ADJOIN[set[nat[x_]]]]]] := 
      True

This function is also finite.

SubstTest[member, domain[funpart[w]], FINITE, 
        w -> composite[ADJOIN[set[nat[x]]], id[P[nat[x]]]]] // 
      Reverse

member[composite[ADJOIN[set[nat[x_]]], id[P[nat[x_]]]], FINITE] := 
      True

The domain and range of a finite bijection have equal cardinality.

SubstTest[implies, and[member[w, BIJ], member[domain[w], FINITE]], 
      equal[card[domain[w]], card[range[w]]], 
      w -> composite[ADJOIN[set[nat[x]]], id[P[nat[x]]]]]

card[
        intersection[complement[P[complement[set[nat[x_]]]]], 
          P[succ[nat[x_]]]]] := card[P[nat[x]]]

The union of the power set of a natural number x and its image under ADJOIN[set[x]] is the power set of succ[x].

SubstTest[image, CUP, 
      cart[P[u], P[v]], {u -> nat[x], v -> set[nat[x]]}]

union[
        intersection[complement[P[complement[set[nat[x_]]]]], 
          P[succ[nat[x_]]]], P[nat[x_]]] := P[succ[nat[x]]]

The image of x under ADJOIN[set[x]] is finite.

SubstTest[member, card[w], omega, 
        w -> intersection[complement[P[complement[set[nat[x]]]]], 
            P[succ[nat[x]]]]] // Reverse

member[
        intersection[complement[P[complement[set[nat[x_]]]]], 
          P[succ[nat[x_]]]], FINITE] := True

The cardinality of the union of two disjoint finite sets is the sum of their cardinalities.

SubstTest[implies, 
      and[disjoint[u, v], member[u, FINITE], member[v, FINITE]], 
      equal[card[union[u, v]], 
        natadd[card[u], card[v]]], 
{u -> 
          intersection[complement[P[complement[set[nat[x]]]]], 
            P[succ[nat[x]]]], v -> P[nat[x]]}]

card[P[succ[nat[x_]]]] := 
      natadd[card[P[nat[x]]], card[P[nat[x]]]]

base case

Lemma.

equal[union[complement[image[V, set[natexp[x, y]]]], natexp[x, y]], 
      natexp[x, y]]

union[complement[image[V, set[natexp[x_, y_]]]], natexp[x_, y_]] := 
      natexp[x, y]

The 0th power of any number is 1.  For a non-number, the 0th power is V.

Map[A, ImageComp[NATEXP, RIGHT[0], set[x]]] // Reverse

natexp[x_, 0] := 
      union[complement[image[V, intersection[omega, set[x]]]], 
        set[0]]

These results suffice for the base case.

equal[card[P[0]], natexp[succ[set[0]], 0]]

induction step

In general, one obtains the next power of a natural number x by multiplying by another factor of x.

SubstTest[natexp, nat[x], natadd[nat[y], z], 
      z -> set[0]]

natexp[nat[x_], succ[nat[y_]]] := 
      natmul[nat[x], natexp[nat[x], nat[y]]]

For the case x = 2, multiplying a number by 2 is equivalent to adding the number to itself.

SubstTest[natexp, nat[w], succ[nat[x]], 
      w -> succ[set[0]]]

natexp[succ[set[0]], succ[nat[x_]]] := 
      natadd[natexp[succ[set[0]], nat[x]], 
        natexp[succ[set[0]], nat[x]]]

induction

To carry out an induction argument using the GOEDEL program, one needs to construct an inductive class.  To construct this class, one can use the fact that the combination of VERTSECT with reify is equivalent to lambda.

VERTSECT[reify[x, card[P[x]]]]

VERTSECT[reify[x, natexp[succ[set[0]], x]]]

One is thus led to consider the following class.

fix[
      composite[inverse[composite[CARD, POWER]], 
        composite[NATEXP, LEFT[succ[set[0]]]]]]

The following membership rule is needed to work with this class.

member[pair[u, v], fix[composite[w, SECOND]]] // AssertTest

member[pair[u_, v_], fix[composite[w_, SECOND]]] := 
      and[member[u, V], member[v, V], 
        member[pair[
            union[v, complement[image[V, set[u]]], 
              complement[image[V, set[v]]]], pair[u, v]], w]]

One also needs a special membership rule for NATEXP.

SubstTest[member, pair[pair[x, y], z], composite[w, id[cart[V, V]]], 
        w -> NATEXP] // Reverse

and[member[x_, V], member[y_, V], member[z_, V], 
        member[pair[pair[x_, y_], z_], NATEXP]] := 
      member[pair[pair[x, y], z], NATEXP]

SubstTest[member, z, image[w, cart[set[x], set[y]]], w -> NATEXP] // 
      Reverse

member[pair[pair[x_, y_], z_], NATEXP] := 
      and[equal[z, natexp[x, y]], member[z, V]]

Finally, one needs to use the fact that any finite set belongs to the class image[Q, OMEGA].

SubstTest[implies, and[member[u, v], subclass[v, w]], 
      member[u, w], 
{u -> P[nat[x]], 
        v -> FINITE, w -> image[Q, OMEGA]}]

member[P[nat[x_]], image[Q, OMEGA]] := True

SubstTest[member, P[nat[y]], image[Q, OMEGA], 
      y -> succ[nat[x]]]

member[P[succ[nat[x_]]], image[Q, OMEGA]] := True

The induction step needs to be rewritten without nat wrappers so that one can eliminate the variables.

SubstTest[implies, equal[x, nat[y]], 
      or[and[equal[card[P[succ[x]]], natexp[succ[set[0]], succ[x]]], 
          member[P[succ[x]], image[Q, OMEGA]]], 
        not[equal[card[P[x]], natexp[succ[set[0]], x]]], not[member[x, V]], 
        not[member[P[x], image[Q, OMEGA]]]], y -> x]

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

At this point, one can eliminate the variable x.

Map[equal[V, #] &, 
        SubstTest[class, x, 
          implies[and[member[x, omega], member[x, y]], member[succ[x], y]], 
          y -> image[fix[composite[inverse[NATEXP], CARD, POWER, SECOND]], 
              set[succ[set[0]]]]]] // Reverse

% /. Equal -> SetDelayed

Applying induction, one finds:

SubstTest[implies, INDUCTIVE[w], 
      subclass[omega, w], 
w -> 
        intersection[omega, 
          image[fix[composite[inverse[NATEXP], CARD, POWER, SECOND]], 
            set[succ[set[0]]]]]]

% /. Equal -> SetDelayed

Finally, variables are reintroduced to obtain the main theorem:

SubstTest[implies, and[member[u, v], subclass[v, w]], 
      member[u, w], 
{u -> nat[x], v -> omega, 
        w -> image[fix[composite[inverse[NATEXP], CARD, POWER, SECOND]], 
            set[succ[set[0]]]]}]

card[P[nat[x_]]] := natexp[succ[set[0]], nat[x]]

variable-free formulation

Lemma.

Map[equal[0, #] &, 
        SubstTest[reify, x, dif[set[P[nat[x]]], y], y -> image[Q, OMEGA]]] // 
      Reverse

% /. Equal -> SetDelayed

Variable-free formulation of the theorem derived in the preceding section.

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

composite[CARD, POWER, id[omega]] := 
      composite[NATEXP, LEFT[succ[set[0]]]]

generalization to arbitrary finite sets

Lemma.

Map[member[fin[y], #] &, ImageComp[Q, id[FINITE], set[nat[x]]]] // 
      Reverse

member[pair[nat[x_], fin[y_]], Q] := 
      equal[card[fin[y]], nat[x]]

More generally, equipollence of finite sets is equivalent to the statement that their cardinalities are equal.

Map[member[fin[y], #] &, ImageComp[Q, id[FINITE], set[fin[x]]]] // 
      Reverse

member[pair[fin[x_], fin[y_]], Q] := 
      equal[card[fin[x]], card[fin[y]]]

Lemma.

SubstTest[member, pair[fin[u], fin[v]], 
        Q, {u -> P[nat[x]], v -> P[fin[y]]}] /. 
      x -> card[fin[y]]

member[pair[P[card[fin[y_]]], P[fin[y_]]], Q] := 
      equal[card[P[fin[y]]], natexp[succ[set[0]], card[fin[y]]]]

Equipollent sets have equipollent power sets.  It follows that the cardinality of the power set of a finite set is equal to 2 raised to the power of the cardinality of the set.

SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, w], 
{u -> pair[nat[x], fin[y]], 
          v -> Q, w -> composite[inverse[POWER], Q, POWER]}] /. 
      x -> card[fin[y]]

card[P[fin[x_]]] := natexp[succ[set[0]], card[fin[x]]]

A variable-free restatement of this general result:

Map[composite[VERTSECT[#], id[FINITE]] &, 
        SubstTest[reify, x, card[P[f[x]]], f -> fin]] // 
      Reverse

composite[CARD, POWER, id[FINITE]] := 
      composite[NATEXP, LEFT[succ[set[0]]], CARD]