closed under finite unions

Johan G. F. Belinfante
2008 January 10

SetDirectory["l:"];  << goedel.08jan06a; << tools.m

summary

In this notebook it is proved that a class is closed under finite unions if and only if it holds the empty set and is closed under binary unions.   The main idea of the derivation is to use FINITE induction:

implies[and[member[0, x], invariant[K, x]], 
      subclass[FINITE, x]]

derivation

The following lemma will be used to simplify the expression that arises when FINITE induction is applied.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], 
{t -> 
            composite[inverse[E], SECOND, id[cart[P[x], V]]], 
          u -> inverse[K], v -> inverse[S]}] // Reverse

subclass[U[image[inverse[K], P[x_]]], x_] := True

Corollary.

equal[intersection[image[K, complement[P[x]]], P[x]], 0]

intersection[image[K, complement[P[x_]]], P[x_]] := 0

Another simplification rule is needed as well:

or[not[member[0, x]], not[subclass[image[CUP, cart[x, x]], x]], 
        subclass[image[CUP, cart[x, union[x, set[0]]]], x]] // 
      AssertTest

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

An image of the cover relation K is rewritten as an image of the function CUP using the following lemma.

Map[
      subclass[image[
            composite[#, 
              composite[id[cart[V, union[set[0], range[SINGLETON]]]], 
                inverse[FIRST]]], image[inverse[BIGCUP], x]], x] &, 
      Assoc[BIGCUP, CUP, id[cart[P[x], P[x]]]]]

subclass[
        image[BIGCUP, 
          intersection[image[K, image[inverse[BIGCUP], x_]], P[x_]]], x_] := 
      subclass[image[CUP, cart[x, union[x, set[0]]]], x]

An application of FINITE induction now yields this:

SubstTest[implies,and[member[0, u], invariant[K, u]],subclass[FINITE, u],
u->union[complement[P[x]], image[inverse[BIGCUP], x]]]//Reverse

Main theorem.

Map[not, 
        SubstTest[and, implies[and[p1, p2], p3], implies[and[p1, p3], p4], 
          not[implies[and[p1, p2], p4]], {p1 -> member[0, x], 
            p2 -> subclass[image[CUP, cart[x, x]], x], 
            p3 -> subclass[image[CUP, cart[x, union[x, set[0]]]], 
                x], 
p4 -> 
              subclass[image[BIGCUP, intersection[FINITE, P[x]]], x]}]] // 
      Reverse

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

The implication in the other direction also holds, and can be combined with the main theorem to obtain the following simple rewrite rule:

equiv[subclass[image[BIGCUP, intersection[FINITE, P[x]]], x], 
      and[member[0, x], subclass[image[CUP, cart[x, x]], x]]]

subclass[image[BIGCUP, intersection[FINITE, P[x_]]], x_] := 
      and[member[0, x], subclass[image[CUP, cart[x, x]], x]]

Corollary.  (Variable-free restatement of the main theorem.)

allclosed[composite[BIGCUP, id[FINITE]]] // Normality

allclosed[composite[BIGCUP, id[FINITE]]] := 
      intersection[binclosed[CUP], 
        complement[P[complement[set[0]]]]]