maximal cliques

Johan G. F. Belinfante
2007 November 25

SetDirectory["l:"]; << goedel99.23b; << tools.m

summary

It is shown in this notebook that the axiom of choice is equivalent to the statement that there are maximal cliques for any small relation.  The axiom of choice is also shown to be equivalent with the stronger statement that for any small relation, every clique is contained in a maximal clique.

derivation

Theorem.

SubstTest[implies, and[subclass[u, v], disjoint[v, w]], 
        disjoint[u, w], {u -> range[CLIQUES], v -> fix[UCHAINS], 
          w -> subvar[inverse[PS]]}] // Reverse

% /. Equal -> SetDelayed

In practice, it is convenient to introduce a variable:

SubstTest[implies, and[member[t, u], implies[p, disjoint[u, v]]], 
        implies[p, not[member[t, v]]], {p -> axch, 
          t -> cliques[setpart[x]], u -> range[CLIQUES], 
          v -> subvar[inverse[PS]]}] // Reverse

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

Theorem. The axiom of choice implies that for any set x, the set cliques[x] has a maximal element.

Map[implies[member[x, y], #] &, 
        SubstTest[implies, equal[x, setpart[t]], 
          or[not[axch], 
            not[subclass[cliques[x], image[inverse[PS], cliques[x]]]]], 
          t -> x]] // Reverse

or[not[axch], not[member[x_, y_]], 
        not[subclass[cliques[x_], image[inverse[PS], cliques[x_]]]]] := 
      True

Corollary.  The axiom of choice implies that for any set x, the set chains[x] has a maximal element.

Map[implies[member[x, y], #] &, 
        SubstTest[or, not[axch], not[member[t, V]], 
          not[subclass[cliques[t], image[inverse[PS], cliques[t]]]], 
          t -> union[x, inverse[x]]]] // Reverse

or[not[axch], not[member[x_, y_]], 
        not[subclass[chains[x_], image[inverse[PS], chains[x_]]]]] := 
      True

negative forms

Theorem.   (A negative form for a special case of Zorn's lemma.)

and[axch, equal[x, Uchains[x]], member[x, y], 
        subclass[x, image[inverse[PS], x]]] // NotNotTest

and[axch, equal[x_, Uchains[x_]], member[x_, y_], 
        subclass[x_, image[inverse[PS], x_]]] := False

Theorem.

and[axch, member[x, y], 
        subclass[cliques[x], image[inverse[PS], cliques[x]]]] // 
      NotNotTest

and[axch, member[x_, y_], 
        subclass[cliques[x_], image[inverse[PS], cliques[x_]]]] := 
      False

Theorem.

and[axch, member[x, y], 
        subclass[chains[x], image[inverse[PS], chains[x]]]] // 
      NotNotTest

and[axch, member[x_, y_], 
        subclass[chains[x_], image[inverse[PS], chains[x_]]]] := 
      False

cross-sections as maximal cliques

Lemma.

AssInt[FUNS, P[cart[V, V]], P[x]]

intersection[FUNS, P[composite[Id, x_]]] := 
      intersection[FUNS, P[x]]

Technical Lemma.

AssInt[image[inverse[IMAGE[id[cart[V, V]]]], FUNS], P[cart[V, V]], 
      P[x]]

intersection[image[inverse[IMAGE[id[cart[V, V]]]], FUNS], 
        P[composite[Id, x_]]] := intersection[FUNS, P[x]]

Lemma.

SubstTest[member, cliques[setpart[t]], range[CLIQUES], 
        t -> intersection[cartsq[composite[Id, setpart[x]]], 
            complement[cross[Id, Di]]]] // Reverse

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

Theorem.  Cross-sections of a class x are maximal elements of the class of functions contained in x.

SubstTest[empty, 
      dif[u, v], {u -> intersection[FUNS, P[x]], 
        v -> image[inverse[PS], intersection[FUNS, P[x]]]}]

subclass[intersection[FUNS, P[x_]], 
        image[inverse[PS], intersection[FUNS, P[x_]]]] := 
      equal[0, X[x]]

converse theorem

Lemma.

SubstTest[implies, and[member[t, u], disjoint[u, v]], 
        not[member[t, v]], 
{t -> 
            intersection[FUNS, P[setpart[x]]], u -> range[CLIQUES], 
          v -> subvar[inverse[PS]]}] // Reverse

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

Converse Theorem.

Map[equal[V, #] &, 
      SubstTest[class, x, 
        implies[empty[u], 
          member[setpart[x], v]], {u -> 
            intersection[range[CLIQUES], subvar[inverse[PS]]], 
          v -> SELECT}]]

% /. Equal -> SetDelayed

Main Theorem.  The axiom of choice is equivalent to the statement that cliques[x] has a maximal element for every set x.

equiv[equal[0, intersection[range[CLIQUES], subvar[inverse[PS]]]], 
      axch]

equal[0, intersection[range[CLIQUES], subvar[inverse[PS]]]] := 
      axch

a stronger version

Theorem.   The axiom of choice implies that every clique of a small relation is contained in a maximal clique.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, 
          w], 
{u -> 
            composite[inverse[E], id[range[CLIQUES]]], 
          v -> composite[inverse[E], 
              id[fix[composite[inverse[IMAGE[inverse[S]]], S, UCHAINS]]]], 
          w -> composite[inverse[S], MAXIMAL[S]]}] // Reverse

% /. Equal -> SetDelayed

Lemma.

Map[empty, 
      dif[intersection[range[CLIQUES], subvar[inverse[PS]]], set[0]] // 
        Renormality]

% /. Equal -> SetDelayed

Converse theorem.  The statement that all cliques of small relations are contained in maximal cliques implies axch.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], 
{t -> FIRST, 
          u -> composite[inverse[E], id[range[CLIQUES]]], 
          v -> composite[inverse[S], MAXIMAL[S]]}] // Reverse

% /. Equal -> SetDelayed

The theorem and its converse can be combined into a single rewrite rule.

equiv[
      subclass[composite[inverse[E], id[range[CLIQUES]]], 
        composite[inverse[S], MAXIMAL[S]]], axch]

subclass[composite[inverse[E], id[range[CLIQUES]]], 
        composite[inverse[S], MAXIMAL[S]]] := axch

introducing variables

A variable can be introduced as follows, using a setpart wrapper:

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
          subclass[u, 
            w], 
{u -> 
              composite[inverse[E], id[set[cliques[setpart[x]]]]], 
            v -> composite[inverse[E], id[range[CLIQUES]]], 
            w -> composite[inverse[S], MAXIMAL[S]]}] // Reverse // 
      MapNotNot

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

Theorem.  If the axiom of choice holds, and if x is a set, then any clique in x is contained in a maximal clique.

Map[implies[member[x, y], #] &, 
        SubstTest[implies, equal[x, setpart[t]], 
          or[not[axch], 
            subclass[cliques[x], 
              image[inverse[S], 
                intersection[cliques[x], 
                  complement[image[inverse[PS], cliques[x]]]]]]], 
          t -> x]] // Reverse

or[not[axch], not[member[x_, y_]], 
        subclass[cliques[x_], 
          image[inverse[S], 
            intersection[cliques[x_], 
              complement[image[inverse[PS], cliques[x_]]]]]]] := 
      True

Hausdorff's maximum principle

Theorem.  If the axiom of choice holds, and if x is a set, then any chain in x is contained in a maximal chain.

Map[implies[member[x, y], #] &, 
        SubstTest[implies, and[axch, member[t, V]], 
          subclass[cliques[t], 
            image[inverse[S], 
              intersection[cliques[t], 
                complement[image[inverse[PS], cliques[t]]]]]], 
          t -> union[x, inverse[x]]]] // Reverse

or[not[axch], not[member[x_, y_]], 
        subclass[chains[x_], 
          image[inverse[S], 
            intersection[chains[x_], 
              complement[image[inverse[PS], chains[x_]]]]]]] := 
      True

Corollary.  The axiom of choice implies Hausdorff's Maximum Principle: every chain of sets in a set x, ordered by inclusion, is contained in a maximal chain.

Map[implies[member[x, y], #] &, 
        SubstTest[implies, and[axch, member[t, V]], 
          subclass[chains[t], 
            image[inverse[S], 
              intersection[chains[t], 
                complement[image[inverse[PS], chains[t]]]]]], 
          t -> composite[id[x], S, id[x]]]] // Reverse

or[not[axch], not[member[x_, y_]], 
        subclass[intersection[chains[S], P[x_]], 
          image[inverse[S], 
            intersection[chains[S], 
              complement[image[inverse[PS], intersection[chains[S], P[x_]]]], 
              P[x_]]]]] := True