maximal elements and funpart

Johan G. F. Belinfante and William Drobny
2008 July 3

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

summary

This notebook is concerned with the formulation of the conclusion of Zorn's lemma for partially ordered sets.  The proof of Zorn's lemma itself is not considered here, and in particular the axiom of choice will not be needed for the results presented here.  The conclusion of Zorn's lemma asserts the existence of a maximal element for certain partially ordered sets.  The GOEDEL program automatically converts the statement of the existence of maximal elements into the following:

member[fix[po[setpart[x]]], domain[MAXIMAL[po[setpart[x]]]]]

Here funpart[x] denotes the function-part of x, that is, its restriction to the class on which x is singlevalued:

class[pair[u, v], equal[image[x, set[u]], set[v]]]

The primary goal of this notebook is to derive rewrite rules that simplify certain more complicated formulations of the maximality condition to the above.  A secondary goal is to derive variable-free formulations of this condition.  The following class is needed for that:

class[x, empty[funpart[x]]]

The double wrapper po[setpart[x]] is used to avoid explicit statements that x is a partial order and a set.  A counterexample is presented to show that for the rewrite rules derived in this notebook the setpart wrapper cannot be omitted.

restrictions of the subset relation

Any restriction of the subset relation S is a partial order.  The GOEDEL program already contains a formulation of Zorn's lemma for this special case:

implies[
      and[axch, member[x, V], subclass[Uchains[x], image[inverse[S], x]]], 
      not[subvariant[inverse[PS], x]]]

For this special case of Zorn's lemma, the existence of maximal elements is formulated as a non-subvariance statement.  In this section, the relation between this statement and the statement involving funpart is investigated.  (In a later section, a more precise connection is established.)

Lemma.

MAXIMAL[composite[id[x], S]] // ReifNormality

MAXIMAL[composite[id[x_], S]] := 
      intersection[
        composite[complement[inverse[E]], IMAGE[inverse[PS]], IMAGE[id[x]]], 
        inverse[E]]

The condition for the existence of a maximal element is now recognized to be equivalent to the non-subvariance statement.

member[x, domain[MAXIMAL[restrict[S, x, x]]]]

The non-subvariance condition  can also be formulated using funpart:

empty[funpart[restrict[S, x, x]]]

The inverse of any partial order is also a partial order.  For restrictions of the inverse of the subset relation, one has:

empty[funpart[restrict[inverse[S], x, x]]]

The above formulas are sufficiently simple that no further rewrite rules are needed for the existence of maximal elements for the special case of restrictions of the subset relation.  There is however an amusing variable-free formula that expresses the connection between these diverse formulations of the maximality condition.  This formula involves the class of all sets lacking maximal elements with respect to the subset relation:

class[x, member[restrict[t, x, x], z]] /. {t -> S, 
        z -> image[inverse[FUNPART], set[0]]}

This expression may be simplified by using Renormality:

fix[
        image[inverse[CART], 
          image[inverse[IMAGE[id[S]]], image[inverse[FUNPART], set[0]]]]] // 
      Renormality

fix[
        image[inverse[CART], 
          image[inverse[IMAGE[id[S]]], image[inverse[FUNPART], set[0]]]]] := 
      subvar[inverse[PS]]

A similar formula holds with S replaced by inverse[S]:

fix[
        image[inverse[CART], 
          image[inverse[IMAGE[id[inverse[S]]]], 
            image[inverse[FUNPART], set[0]]]]] // Renormality

fix[
        image[inverse[CART], 
          image[inverse[IMAGE[id[inverse[S]]]], 
            image[inverse[FUNPART], set[0]]]]] := subvar[PS]

a funpart saga

The function funpart[x] is a restriction of x:

composite[x, id[domain[funpart[x]]]]

For a composite relation, one has:

SubstTest[funpart, composite[x, y, id[z]], 
      z -> domain[funpart[y]]]

composite[funpart[composite[x_, y_]], id[domain[funpart[y_]]]] := 
      composite[funpart[x], funpart[y]]

Corollary.

SubstTest[implies, equal[u, v], 
        equal[composite[u, w], 
          composite[v, w]], {u -> funpart[composite[funpart[x], y]], 
          v -> 0, w -> id[domain[funpart[y]]]}] // 
      Reverse

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

For the next theorem, the usual method of proving theorems using SubstTest had to be altered slightly to accomodate the following rewrite rule:

and[subclass[u, v], disjoint[u, v]]

Theorem.   (Comment. The above rewrite rule applies to the combination and[p3, p4] here.)

SubstTest[and, implies[p1, p3], 
        implies[p2, p4], {p1 -> subclass[range[y], domain[funpart[x]]], 
          p2 -> equal[0, funpart[composite[funpart[x], y]]], 
          p3 -> subclass[range[funpart[y]], domain[funpart[x]]], 
          p4 -> equal[0, 
              intersection[domain[funpart[x]], range[funpart[y]]]]}] // 
      MapNotNot

or[equal[0, funpart[y_]], 
        not[equal[0, funpart[composite[funpart[x_], y_]]]], 
        not[subclass[range[y_], domain[funpart[x_]]]]] := True

Lemma.  (Application of the above lemma to partial orders.)

SubstTest[implies, 
        and[equal[0, funpart[composite[funpart[u], v]]], 
          subclass[range[v], domain[funpart[u]]]], 
        equal[0, 
          funpart[v]], {u -> 
            composite[VERTSECT[inverse[po[setpart[x]]]], 
              id[fix[po[setpart[x]]]]], v -> po[setpart[x]]}] // 
      Reverse

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

A series of lemmas is needed to derive the converse statement.

Lemma.

SubstTest[or, equal[0, funpart[v]], 
        not[equal[0, funpart[composite[funpart[u], v]]]], 
        not[subclass[range[v], domain[funpart[u]]]], {u -> 
            inverse[oopart[x]], v -> composite[oopart[x], y]}] // 
      Reverse

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

Lemma.

SubstTest[implies, and[empty[funpart[u]], equal[u, v]], 
        empty[funpart[v]], 
{u -> composite[Id, y], 
          v -> composite[id[domain[oopart[x]]], y]}] // Reverse

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

Theorem.   Combining these two lemmas yields:

Map[not, 
        SubstTest[and, implies[and[p1, p2], p3], implies[p3, p4], 
          not[implies[and[p1, p2], p4]], {p1 -> empty[funpart[y]], 
            p2 -> subclass[range[y], domain[oopart[x]]], 
            p3 -> equal[0, funpart[composite[id[domain[oopart[x]]], y]]], 
            p4 -> equal[0, funpart[composite[oopart[x], y]]]}]] // 
      Reverse

or[equal[0, funpart[composite[oopart[x_], y_]]], 
        not[equal[0, funpart[y_]]], 
        not[subclass[range[y_], domain[oopart[x_]]]]] := True

Lemma.   Application to obtain a desired converse of the statement about partial orders.

SubstTest[implies, 
        and[equal[0, funpart[v]], subclass[range[v], domain[oopart[u]]]], 
        equal[0, 
          funpart[composite[oopart[u], v]]], {u -> 
            composite[VERTSECT[inverse[po[setpart[x]]]], 
              id[fix[po[setpart[x]]]]], v -> po[setpart[x]]}] // 
      Reverse

or[equal[0, 
          funpart[composite[VERTSECT[inverse[po[setpart[x_]]]], 
              po[setpart[x_]]]]], not[equal[0, funpart[po[setpart[x_]]]]]] := 
      True

Main Theorem.  (A simplification rule for a maximality statement about partial orders.

equiv[
      equal[0, funpart[
          composite[VERTSECT[inverse[po[setpart[x]]]], po[setpart[x]]]]], 
      equal[0, funpart[po[setpart[x]]]]]

equal[0, 
        funpart[composite[VERTSECT[inverse[po[setpart[x_]]]], 
            po[setpart[x_]]]]] := 
      equal[0, funpart[po[setpart[x]]]]

counterexample

Comment.  The following counterexample shows that the setpart wrapper can not be omitted from the main theorem in the preceding section.

equiv[equal[0, funpart[composite[VERTSECT[inverse[po[x]]], po[x]]]], 
        equal[0, funpart[po[x]]]] /. x -> inverse[S]

existence of maximal elements for posets

In this section yet another formulation of the existence of maximal elements is derived for the case of partially ordered sets.  The result derived in this section is needed to derive the general statement of Zorn's lemma for partially ordered sets from the special case of restrictions of the subset relation that is already available.  To do this, one needs to use the fact that any partial order is isomorphic to a restriction of the subset relation.  An explicit formula for one such isomorphism is

APPLY[VS, inverse[po[setpart[x]]]]

A precise statement of the isomorphism can be formulated as follows:

implies[equal[t, APPLY[VS, inverse[po[setpart[x]]]]], 
      equal[composite[t, po[setpart[x]], inverse[t]], 
        restrict[S, range[t], range[t]]]]

Technical Lemma.   (Another simplification rule obtained using  po[x] = po[x] ∘ id[fix[po[x]]].)

Map[empty, 
      SubstTest[funpart, 
        composite[u, 
          id[v]], {u -> 
            composite[VERTSECT[inverse[po[setpart[x]]]], po[setpart[x]]], 
          v -> fix[po[setpart[x]]]}]]

equal[0, 
        intersection[
          domain[funpart[
              composite[VERTSECT[inverse[po[setpart[x_]]]], 
                po[setpart[x_]]]]], fix[po[setpart[x_]]]]] := 
      equal[0, funpart[po[setpart[x]]]]

Lemma.  (An implication in one direction.)

Map[
        implies[empty[#], 
            equal[0, 
              funpart[composite[VERTSECT[inverse[po[setpart[x]]]], 
                  po[setpart[x]]]]]] &, 
        SubstTest[funpart, 
          composite[inverse[oopart[w]], po[setpart[x]], 
            oopart[w]], 
{w -> 
              composite[id[fix[po[setpart[x]]]], 
                inverse[VERTSECT[inverse[po[setpart[x]]]]]]}]] // 
      Reverse

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

Lemma.  (Implication in the reverse direction.)

Map[
        revimp[empty[#], 
            equal[0, 
              funpart[composite[VERTSECT[inverse[po[setpart[x]]]], 
                  po[setpart[x]]]]]] &, 
        SubstTest[funpart, 
          composite[inverse[oopart[w]], po[setpart[x]], 
            oopart[w]], 
{w -> 
              composite[id[fix[po[setpart[x]]]], 
                inverse[VERTSECT[inverse[po[setpart[x]]]]]]}]] // 
      Reverse

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

Theorem.    Combining the preceding two lemmas yields a logical equivalence that can be made into a simplification rewrite rule for the existence of maximal elements of posets.

equiv[
      subclass[image[VERTSECT[inverse[po[setpart[x]]]], fix[po[setpart[x]]]], 
        image[inverse[PS], 
          image[VERTSECT[inverse[po[setpart[x]]]], fix[po[setpart[x]]]]]], 
      equal[0, funpart[po[setpart[x]]]]]

subclass[
        image[VERTSECT[inverse[po[setpart[x_]]]], fix[po[setpart[x_]]]], 
        image[inverse[PS], 
          image[VERTSECT[inverse[po[setpart[x_]]]], fix[po[setpart[x_]]]]]] := 
      equal[0, funpart[po[setpart[x]]]]

counterexample

Comment.  The following counterexample shows that the setpart wrapper can not be omitted from the simplification rule derived in the preceding section.

equiv[
        subclass[image[VERTSECT[inverse[po[x]]], fix[po[x]]], 
          image[inverse[PS], image[VERTSECT[inverse[po[x]]], fix[po[x]]]]], 
        equal[0, funpart[po[x]]]] /. x -> inverse[S]