cliques families

Johan G. F. Belinfante
2010 August 14

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

summary

Rewrite rules for cliques families are derived, generalizing similar formulas discovered in 2003 for the special case of function families.

function families

A curious formula for function families was derived 2003 June 5.  A function family is a relation whose vertical sections are all functions.  The GOEDEL program does not retain a separate predicate for this because it can transform this to a statement involving existing concepts:

assert[forall[y, FUNCTION[image[x, set[y]]]]]

Function families were also studied using William McCune’s automated reasoning program Otter.   A different definition of function family was used in the Otter work, which the GOEDEL program rewrites using this rule:

range[complement[composite[E, complement[x]]]]

It was shown in 2003 that the two definitions coincide, resulting in the following rewrite rule:

subclass[domain[LB[x]], FUNS]

A similar rule holds with LB replaced by UB.

subclass[domain[UB[x]], FUNS]

Two new rules of a similar nature can be derived.

Theorem.

SubstTest[subclass, image[INVERSE, u], 
        image[INVERSE, v], {u -> domain[UB[x]], 
          v -> image[INVERSE, FUNS]}] // Reverse

subclass[image[INVERSE, domain[UB[x_]]], FUNS] := 
      FUNCTION[rotate[composite[x, SWAP]]]

Corollary.

SubstTest[subclass, image[INVERSE, domain[UB[t]]], FUNS, 
        t -> inverse[x]] // Reverse

subclass[image[INVERSE, domain[LB[x_]]], FUNS] := 
      FUNCTION[rotate[composite[inverse[x], SWAP]]]

cliques families

In this notebook the more general concept of a cliques family is studied.  The statement that every vertical section of  x  is a clique for  y  is transformed by the GOEDEL program as follows:

assert[forall[t, subclass[P[image[x, set[t]]], cliques[y]]]]

The following theorem yields a rewrite rule that transforms an equivalent statement, generalizing the rewrite rule discovered in 2003.

Theorem.

SubstTest[assert, forall[t, subclass[P[image[x, set[t]]], z]], 
      z -> cliques[y]]

subclass[domain[LB[x_]], cliques[y_]] := 
      subclass[composite[x, inverse[x]], y]

Corollary.

SubstTest[subclass, domain[LB[t]], cliques[y], t -> inverse[x]] // 
      Reverse

subclass[domain[UB[x_]], cliques[y_]] := 
      subclass[composite[inverse[x], x], y]

special cases

The following special cases are of interest.

Theorem.

SubstTest[subclass, domain[LB[x]], cliques[y], y -> Id] // 
      Reverse

subclass[domain[LB[x_]], union[range[SINGLETON], set[0]]] := 
      FUNCTION[composite[Id, x]]

Theorem.

SubstTest[subclass, domain[UB[x]], cliques[y], y -> Id] // 
      Reverse

subclass[domain[UB[x_]], union[range[SINGLETON], set[0]]] := 
      FUNCTION[inverse[x]]

Another case of interest is this:

Theorem.

SubstTest[subclass, domain[UB[x]], cliques[y], y -> Di] // 
      Reverse

subclass[domain[UB[x_]], set[0]] := equal[0, domain[x]]

Corollary.

equal[domain[UB[x]], set[0]] // AssertTest

equal[domain[UB[x_]], set[0]] := equal[0, domain[x]]

Corollary.

SubstTest[equal, domain[UB[t]], set[0], t -> inverse[x]] // 
      Reverse

equal[domain[LB[x_]], set[0]] := equal[0, domain[x]]