the class of partitions

Johan G. F. Belinfante
2010 January 5

SetDirectory["l:"]; << goedel.10jan04a; << tools.m

summary

A partition x of a class y is a pairwise disjoint collection of nonempty subsets of y whose sum class is y.  Since y = U[x], one can dispense with the variable y altogether, and work with just the single variable x.  The class PARTNS of all (small) partitions will accordingly be defined as the class of all pairwise disjoint sets that do not hold the empty set.

member[x_, PARTNS] := 
      and[member[x, V], not[member[0, x]], 
        subclass[cart[x, x], union[DISJOINT, Id]]]

In this notebook, some basic properties of this class are derived.

normalization

The class PARTNS is normalized by the following rewrite rule.

Theorem.  Normalization rule.

PARTNS // Normality // Reverse

intersection[cliques[union[DISJOINT, Id]], P[complement[set[0]]]] := 
      PARTNS

Corollary.  Partitions are pairwise disjoint sets.

SubstTest[subclass, intersection[u, v], 
        u, {u -> cliques[union[DISJOINT, Id]], v -> P[complement[set[0]]]}] // 
      Reverse

subclass[PARTNS, cliques[union[DISJOINT, Id]]] := True

CORE[PARTNS]

Theorem.  The sum class of PARTNS is the class of non-empty sets.

SubstTest[U, 
        intersection[u, P[v]], {u -> cliques[union[DISJOINT, Id]], 
          v -> complement[set[0]]}] // Reverse

U[PARTNS] := complement[set[0]]

A similar result holds for core.

Lemma.

AssInt[cliques[union[DISJOINT, Id]], P[complement[set[0]]], 
      P[x]]

intersection[cliques[union[DISJOINT, Id]], 
        P[intersection[x_, complement[set[0]]]]] := 
      intersection[PARTNS, P[x]]

Theorem.

SubstTest[U, 
        intersection[u, P[v]], {u -> cliques[union[DISJOINT, Id]], 
          v -> intersection[x, complement[set[0]]]}] // 
      Reverse

core[PARTNS, x_] := intersection[x, complement[set[0]]]

Corollary.

Map[VERTSECT, 
      SubstTest[reify, x, core[t, x], t -> PARTNS]]

CORE[PARTNS] := IMAGE[id[complement[set[0]]]]

other properties of the class of partitions

Although the class PARTNS only holds partitions which are sets, it is also useful for partitions that are proper classes.

Theorem.  A class x is a (possibly large) partition if and only if P[x] ⊂ PARTNS.

SubstTest[subclass, t, 
        intersection[u, v], {t -> P[x], 
          u -> cliques[union[DISJOINT, Id]], v -> P[complement[set[0]]]}] // 
      Reverse

subclass[P[x_], PARTNS] := 
      and[not[member[0, x]], 
        subclass[cart[x, x], union[DISJOINT, Id]]]

Theorem.  The class PARTNS is a class of the form cliques[x] for the restriction of  DISJOINT ⋃ Id to the class of all nonempty sets.

SubstTest[cliques, 
        intersection[u, v], {u -> union[DISJOINT, Id], 
          v -> cartsq[complement[set[0]]]}] // Reverse

cliques[
        union[composite[id[complement[set[0]]], DISJOINT, 
            id[complement[set[0]]]], id[complement[set[0]]]]] := 
      PARTNS

Corollary.  The class of partitions is hereditary.

SubstTest[image, inverse[S], cliques[x], 
        x -> union[
            composite[id[complement[set[0]]], DISJOINT, 
              id[complement[set[0]]]], id[complement[set[0]]]]] // 
      Reverse

image[inverse[S], PARTNS] := PARTNS

Corollary.  The class of partitions is closed under arbitrary intersections.  No new rewrite rule is needed for this.

Aclosure[PARTNS]

Corollary.  The union of a chain of partitions is a partition.

SubstTest[Uchains, cliques[x], 
        x -> union[
            composite[id[complement[set[0]]], DISJOINT, 
              id[complement[set[0]]]], id[complement[set[0]]]]] // 
      Reverse

Uchains[PARTNS] := PARTNS

The class of partitions is not closed under arbitrary unions.  In fact, any set of nonempty sets is the sum class of a set of partitions.    No new rewrite rule is needed for this.

Uclosure[PARTNS]

replacement rules

Some old rules can be replaced with the rules derived in this section.

Theorem.

Map[
      equal[V, #] &, dif[PARTNS, 
            fix[composite[DISJOINT, IMAGE[inverse[PS]]]]] // complement // 
        Normality]

subclass[PARTNS, fix[composite[DISJOINT, IMAGE[inverse[PS]]]]] := 
      True

Lemma.  Every set can be partitioned.

(SubstTest[implies, member[u, v], 
            not[empty[v]], {u -> image[SINGLETON, t], 
              v -> 
                intersection[PARTNS, image[inverse[BIGCUP], set[t]]]}] // 
          Reverse) /. t -> setpart[x]

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

Theorem.

SubstTest[class, x, member[setpart[x], t], 
      t -> image[BIGCUP, PARTNS]]

image[BIGCUP, PARTNS] := V