λx. cover[x]

Johan G. F. Belinfante
2010 January 29

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

summary

The function COVER = λx. cover[x] is defined in this notebook, and some of its properties are derived.

reify rule for cover[x]

Reification is an important tool for eliminating set variables.  A reify rule for the constructor cover[x] is needed.

Theorem.  Reify rule for cover[x].

SubstTest[reify, x, dif[g[x], composite[g[x], g[x]]], 
        g[x] -> intersection[Di, f[x]]] // Reverse

reify[x_, cover[y_]] := 
      composite[id[Di], 
        intersection[
          composite[SWAP, 
            complement[
              composite[RIF, id[cart[Di, Di]], 
                intersection[composite[inverse[FIRST], reify[x, y]], 
                  composite[inverse[SECOND], reify[x, y]]]]]], 
          reify[x, y]]]

definition of COVER

Definition.   The class COVER is defined by the following membership rule.

member[x_, COVER] := 
      and[member[first[x], V], equal[second[x], cover[first[x]]]]

Lemma.  The class COVER is a relation.

Map[empty, dif[COVER, cart[V, V]] // Normality]

subclass[COVER, cart[V, V]] := True

Lemma.  Simplification rule.

equal[composite[Id, COVER], COVER]

composite[Id, COVER] := COVER

normalization rule

Some simplification rules are needed to clean up the normalization rule for COVER.  In the final section of this notebook a more general simplification rule is derived.

Lemma.  Simplification rule.

composite[SWAP, complement[inverse[E]], COMPOSE, DUP, IMAGE[SWAP], 
        IMAGE[id[Di]]] // DoubleComplement

% /. Equal -> SetDelayed

Lemma.  Simplification rule.

SubstTest[VERTSECT, 
        dif[thinpart[x], thinpart[y]], {x -> inverse[E], 
          y -> 
            complement[
              composite[complement[inverse[E]], COMPOSE, DUP, 
                IMAGE[id[Di]]]]}] // Reverse

% /. Equal -> SetDelayed

Theorem. (Normalization rule.)  This explicit formula for COVER will be used to derive many of its properties.

Map[reify[x, #] &, image[COVER, set[setpart[x]]] // Normality] // 
      Reverse

composite[DIF, id[composite[IMAGE[id[Di]], COMPOSE, DUP]], 
        inverse[FIRST], IMAGE[id[Di]]] := COVER

Corollary.

Assoc[
        composite[DIF, id[composite[IMAGE[id[Di]], COMPOSE, DUP]], 
          inverse[FIRST]], IMAGE[id[Di]], IMAGE[id[Di]]] // 
      Reverse

composite[COVER, IMAGE[id[Di]]] := COVER

an upper bound for COVER

An upper bound for COVER follows as an immediate application of the normalization rule for COVER.

Theorem.

SubstTest[subclass, composite[x, id[t], y], 
        composite[x, y], {t -> composite[IMAGE[id[Di]], COMPOSE, DUP], 
          x -> DIF, 
          y -> composite[inverse[FIRST], IMAGE[id[Di]]]}] // 
      Reverse

subclass[COVER, composite[inverse[S], IMAGE[id[Di]]]] := 
      True

Corollary.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> COVER, 
          v -> composite[inverse[S], IMAGE[id[Di]]], w -> inverse[S]}] // 
      Reverse

subclass[COVER, inverse[S]] := True

basic properties of COVER

Theorem.  The relation COVER is a function.

SubstTest[FUNCTION, 
        composite[DIF, id[composite[IMAGE[id[Di]], COMPOSE, DUP]], 
          inverse[FIRST], funpart[t]], t -> IMAGE[id[Di]]] // 
      Reverse

FUNCTION[COVER] := True

Theorem.  The function COVER is total.

SubstTest[domain, composite[DIF, id[x], inverse[FIRST], IMAGE[id[Di]]], 
        x -> composite[IMAGE[id[Di]], COMPOSE, DUP]] // Reverse

domain[COVER] := V

Corollary.  The function COVER is a proper class.

Map[not, 
        SubstTest[implies, equal[V, domain[t]], not[member[t, x]], 
          t -> COVER]] // Reverse

member[COVER, x_] := False

vertical section rule

An APPLY rule for COVER is first derived with a setpart wrapper.  Later, a more general rule is derived, and from it a vertical section rule.

Lemma.  Sethood rule.

SubstTest[implies, and[subclass[u, v], member[v, V]], 
        member[u, V], {u -> cover[setpart[x]], v -> setpart[x]}] // 
      Reverse

member[cover[setpart[x_]], V] := True

Lemma.  (Temporary rewrite rule, to be replaced shortly.)

ApComp[
        composite[DIF, id[composite[IMAGE[id[Di]], COMPOSE, DUP]], 
          inverse[FIRST]], IMAGE[id[Di]], setpart[x]] // Reverse

APPLY[COVER, setpart[x_]] := cover[setpart[x]]

Lemma.   (Removing the setpart wrapper.)

SubstTest[implies, equal[x, setpart[t]], 
        equal[APPLY[COVER, x], cover[x]], t -> x] // Reverse

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

Theorem.  General APPLY rule for COVER.

equal[APPLY[COVER, x], 
      union[complement[image[V, set[x]]], cover[x]]]

APPLY[COVER, x_] := 
      union[complement[image[V, set[x]]], cover[x]]

Theorem.   Vertical section rule.

SubstTest[image, funpart[t], set[x], t -> COVER] // 
      Reverse

image[COVER, set[x_]] := 
      intersection[image[V, set[x]], set[cover[x]]]

idempotence and duality

One can use FastReifNormality to derive the following properties of the function COVER.

Theorem.  Idempotent property.

composite[COVER, COVER] // FastReifNormality

composite[COVER, COVER] := COVER

Theorem.  The function COVER commutes with IMAGE[SWAP].

composite[COVER, IMAGE[SWAP]] // FastReifNormality

composite[COVER, IMAGE[SWAP]] := 
      composite[IMAGE[SWAP], COVER]

U[range[COVER]]

In this section, a formula for U[range[COVER]] is derived.

Theorem.  The cover relation of any relation is irreflexive.

composite[IMAGE[id[Di]], COVER] // FastReifNormality

composite[IMAGE[id[Di]], COVER] := COVER

Corollary.  The class U[range[COVER]] is a relation.

Map[subclass[U[#], cart[V, V]] &, 
      ImageComp[IMAGE[id[Di]], COVER, V]]

% /. Equal -> SetDelayed

Corollary. The relation U[range[COVER]] is irreflexive.

Map[fix[U[#]] &, ImageComp[IMAGE[id[Di]], COVER, V]]

% /. Equal -> SetDelayed

To obtain a lower bound, the special case of a singleton relation will suffice.

Lemma.  Cover relation of a singleton.

cover[cart[set[x], set[y]]] // VSNormality

cover[cart[set[x_], set[y_]]] := 
      cart[intersection[complement[set[y]], set[x]], set[y]]

Lemma.   Lower bound for U[range[COVER]].

Map[subclass[U[range[#]], U[range[COVER]]] &, 
        composite[COVER, SINGLETON] // FastReifNormality] // 
      Reverse

% /. Equal -> SetDelayed

Theorem.  A formula for U[range[COVER]].

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> U[range[COVER]], v -> Di}]

U[range[COVER]] := Di

cover relations of total orders

Theorem.  The cover relation of a total order is a function.

Map[equal[V, #] &, 
      SubstTest[class, x, 
        implies[member[x, t], 
          subclass[P[APPLY[funpart[v], x]], u]], {t -> TO, 
          u -> FUNS, v -> COVER}]]

subclass[image[COVER, TO], FUNS] := True

Corollary.  The cover relation of a wellorder relation is a function.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> WO, v -> TO, 
          w -> image[inverse[COVER], FUNS]}] // Reverse

subclass[image[COVER, WO], FUNS] := True

cover relations of well-founded relations

Variable-free reformulations are derived for the domain of the cover relation of a small well-founded relation and for a small well-order relation.

Lemma.  (Removing the compound wrapper  wf[setpart[x]]  from an existing rewrite rule.)

Map[implies[member[x, y], #] &, 
        SubstTest[implies, equal[x, wf[setpart[t]]], 
          equal[domain[cover[x]], domain[x]], t -> x]] // 
      Reverse

or[equal[domain[x_], domain[cover[x_]]], not[member[x_, y_]], 
        not[WELLFOUNDED[x_]]] := True

Lemma.  (Elimination of a set variable using class rules.)

Map[equal[V, #] &, 
      SubstTest[class, t, 
        implies[member[t, w], 
          equal[domain[APPLY[funpart[v], t]], domain[t]]], {v -> COVER, 
          w -> WF}]]

% /. Equal -> SetDelayed

This variable-free result can be cast in a more elegant form.

Lemma.  An inclusion.

SubstTest[implies, subclass[u, v], 
        subclass[composite[t, u], composite[t, v]], {t -> IMAGE[FIRST], 
          u -> id[WF], 
          v -> composite[inverse[IMAGE[FIRST]], IMAGE[FIRST], COVER]}] // 
      Reverse

% /. Equal -> SetDelayed

Inclusions for functions can always be replaced by equations, because any subclass of a function is a restriction of that function.

Theorem.   Variable-free equational restatement of the formula  domain[cover[x]] = domain[x] for x ∈ WF.

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
        equal[u, 
          composite[v, id[domain[u]]]], {u -> 
            composite[IMAGE[FIRST], id[WF]], 
          v -> composite[IMAGE[FIRST], COVER]}] // Reverse

composite[IMAGE[FIRST], COVER, id[WF]] := 
      composite[IMAGE[FIRST], id[WF]]

A variable-free equational restatement of a formula fort the domain of the cover relation of small well-ordering will now be derived by using the fact that if  w  is a well-ordering, then  Di ⋂ w  is a well-founded relation.  One can do this directly without reintroducing variables.

Lemma.  Simplification rule.

equal[intersection[image[IMAGE[id[Di]], WO], WF], 
      image[IMAGE[id[Di]], WO]]

intersection[WF, image[IMAGE[id[Di]], WO]] := 
      image[IMAGE[id[Di]], WO]

Corollary.   Variable-free restatement of the formula  domain[cover[x]] = fix[Di ∘ x] for x ∈ WO.

Map[composite[#, IMAGE[id[Di]], id[WO]] &, 
      Assoc[composite[IMAGE[FIRST], COVER], id[WF], 
        id[image[IMAGE[id[Di]], WO]]]]

composite[IMAGE[FIRST], COVER, id[WO]] := 
      composite[IMAGE[FIRST], IMAGE[id[Di]], id[WO]]

a general simplification rule

The following rewrite rule was not used, but is closely related to the normalization rule for COVER.

Theorem.   Simplification rule.

SubstTest[VERTSECT, 
        dif[thinpart[u], thinpart[v]], {u -> inverse[E], 
          v -> composite[inverse[E], COMPOSE, DUP]}] // Reverse

A more general result will now be derived that subsumes this rewrite rule.  The idea is to replace the specific function COMPOSE ∘ DUP with a generic function funpart[t].  In general, however, this produces a big mess.

Lemma.

Map[
        implies[equal[domain[funpart[t]], V], 
            equal[#, composite[DIF, id[funpart[t]], inverse[FIRST]]]] &, 
        SubstTest[VERTSECT, 
          dif[thinpart[u], thinpart[v]], {u -> inverse[E], 
            v -> composite[inverse[E], funpart[t]]}]] // Reverse

(% /. t -> t_) /. Equal -> SetDelayed

The lemma can be cleaned up by adding the hypothesis that the function be total.

Theorem.

SubstTest[implies, equal[v, domain[funpart[t]]], 
        or[equal[composite[DIF, id[funpart[t]], inverse[FIRST]], 
            union[composite[
                VERTSECT[
                  intersection[composite[complement[inverse[E]], funpart[t]], 
                    inverse[E]]], id[v]], 
              composite[CUP, 
                id[composite[
                    VERTSECT[
                      intersection[
                        composite[complement[inverse[E]], funpart[t]], 
                        inverse[E]]], id[complement[v]]]], inverse[FIRST]]]], 
          not[equal[V, v]]], v -> V] // Reverse

(% /. t -> t_) /. Equal -> SetDelayed

The funpart wrapper can be removed.

SubstTest[implies, equal[x, funpart[t]], 
        or[equal[composite[DIF, id[x], inverse[FIRST]], 
            VERTSECT[
              intersection[composite[complement[inverse[E]], x], 
                inverse[E]]]], not[equal[V, domain[x]]]], t -> x] // 
      Reverse

or[equal[composite[DIF, id[x], inverse[FIRST]], 
          VERTSECT[
            intersection[composite[complement[inverse[E]], x], inverse[E]]]], 
        not[equal[V, domain[x_]]], not[FUNCTION[x_]]] := True

Restatement.

implies[and[FUNCTION[x], equal[V, domain[x]]], 
      equal[VERTSECT[
          intersection[composite[complement[inverse[E]], x], inverse[E]]], 
        composite[DIF, id[x], inverse[FIRST]]]]

Finally, this can be made into a conditional rewrite rule.

VERTSECT[
        intersection[composite[complement[inverse[E]], x_], inverse[E]]] := 
      composite[DIF, id[x], inverse[FIRST]] /; 
        and[FUNCTION[x], equal[V, domain[x]]]