erasing

Johan G. F. Belinfante
2007 October 18

SetDirectory["l:"];  << goedel98.16a;  <<  tools.m

summary

Given a set x, one can erase parts of it in various ways to obtain a subset y.  For each type of erasure it is interesting to study its erasure relation consisting of all ordered pairs pair[x, y]  such that y can be obtained from x by erasure in a specified way.   If no restriction whatsoever is placed on the erasure process, so that any subset can be obtained, the erasure relation is just the inverse of the subset relation S.

class[pair[x, y], subclass[y, x]]

An important type of erasure in the theory of relations is restriction.  By erasing vertically, one can obtain from a given relation x its restrictions, that is, subrelations of the form composite[x, id[v]].   The erasure relation for this type of erasure has a special name in the GOEDEL program:

class[pair[x, y], 
      assert[exists[v, equal[y, composite[x, id[v]]]]]]

Erasing both horizontally and vertically yields relations of the form composite[id[u], x, id[v]].  For the theory of partial orders, the symmetric case u = v is important.  The erasure relations for each of these types of erasures may have formal properties such as transitivity, for which one can derive rewrite rules. It would also be desirable to have rewrite rules to help reduce the myriad formulas for specific erasure processes to obtain standard forms by which one can refer to them.   Many types of erasure have special names, but it is probably best to be conservative about the number of new names to be introduced inro the GOEDEL program, partly because the names are not completely standard, but also because there may be rewrite rules common to several forms of erasure.  Introducing separate names for all the various forms of erasure would introduce unnecessary duplication.

introduction

Lemma.

composite[CAP, id[cart[V, x]], inverse[FIRST]] // VSNormality // 
      Reverse

intersection[fix[composite[inverse[DIF], DISJOINT, id[x_], S, SECOND]], 
        inverse[S]] := 
      composite[CAP, id[cart[V, x]], inverse[FIRST]]

The types of erasure considered in the present notebook are mainly of the general form y = intersection[x, t] where t can be any member of some specified class z.  The corresponding erasure relation is:

class[pair[x, y], 
        exists[t, and[member[t, z], equal[y, intersection[x, t]]]]]

A slight generalization of this is obtained by requiring the set x to belong to a specified class w.

class[pair[x, y], 
        and[member[x, w], 
          exists[t, and[member[t, z], equal[y, intersection[x, t]]]]]]

One could of course consider still more general erasure relations of the form composite[CAP, id[x], inverse[FIRST]], but most of the rewrite rules derived below fail at this higher level of generality.  The rules derived in the next section are an exception to this.

antisymmetry

Lemma.

fix[composite[inverse[CAP], inverse[S], FIRST]] // 
      InvertFixTest

fix[composite[inverse[CAP], inverse[S], FIRST]] := 
      cart[V, V]

Theorem.

subclass[composite[FIRST, id[x], inverse[CAP]], S] // 
      AssertTest

subclass[composite[FIRST, id[x_], inverse[CAP]], S] := True

Corollary.  Any subclass of S is an antisymmetric relation.  The following rewrite rule is slightly more general than necessary:

SubstTest[subclass, w, 
        intersection[u, 
          v], {w -> intersection[composite[CAP, id[x], inverse[FIRST]], 
              composite[FIRST, id[y], inverse[CAP]]], u -> S, 
          v -> inverse[S]}] // Reverse

subclass[
        intersection[composite[CAP, id[x_], inverse[FIRST]], 
          composite[FIRST, id[y_], inverse[CAP]]], Id] := True

normalization

The GOEDEL program already contains the following rewrite rule for standardizing one variant expression for the type of erasure under consideration:

composite[CAP, id[cart[x, y]], inverse[SECOND]]

Other formulas can be derived using various Normality tests.  Some of these may strike one as somewhat strange;  for example:

(composite[CAP, id[x], inverse[FIRST]] // ReifNormality // 
          Reverse) /. x -> V

composite[IMG, inverse[FIRST], IMAGE[DUP]] := inverse[S]

The use of ReifNormality yields this rewrite rule:

composite[CAP, id[cart[V, x]], inverse[FIRST]] // ReifNormality // 
      Reverse

composite[IMG, id[cart[V, x_]], inverse[FIRST], IMAGE[DUP]] := 
      composite[CAP, id[cart[V, x]], inverse[FIRST]]

Yet another such expression is this:

intersection[
        composite[SECOND, id[composite[inverse[S], id[x]]], inverse[DIF], 
          DISJOINT], inverse[S]] // ReifNormality

intersection[
        composite[SECOND, id[composite[inverse[S], id[x_]]], inverse[DIF], 
          DISJOINT], inverse[S]] := 
      composite[CAP, id[cart[V, x]], inverse[FIRST]]

And here is still one more:

composite[IMG, id[cart[image[IMAGE[DUP], x], V]], inverse[SECOND]] // 
      ReifNormality

composite[IMG, id[cart[image[IMAGE[DUP], x_], V]], inverse[SECOND]] := 
      composite[CAP, id[cart[V, x]], inverse[FIRST]]

composite erasures

In general one could perform two types of erasures, one after the other, say with parameters x and y.  For the types of erasure under consideration, the composite is again an erasure of the type under consideration with parameter image[CAP, cart[x, y]].  Note that the order is not important because the symmetry of the function CAP inplies that this expression is symmetric in x and y.  A slightly more general rule can be derived:

Assoc[CAP, composite[cross[Id, CAP], ASSOC], 
        composite[composite[id[cart[cart[x, y], z]], inverse[FIRST]], 
          inverse[FIRST]]] // Reverse

composite[CAP, id[cart[V, z_]], inverse[FIRST], CAP, id[cart[x_, y_]], 
        inverse[FIRST]] := 
      composite[CAP, id[cart[x, image[CAP, cart[y, z]]]], 
        inverse[FIRST]]

transitive laws

Lemma.

SubstTest[implies, subclass[x, y], subclass[image[t, x], image[t, y]], 
        t -> composite[
            intersection[composite[inverse[FIRST], inverse[w]], 
              composite[inverse[SECOND], u]], id[cart[v, V]], 
            inverse[SECOND]]] // Reverse

or[not[subclass[x_, y_]], 
        subclass[composite[u_, id[cart[v_, x_]], w_], 
          composite[u_, id[cart[v_, y_]], w_]]] := True

Theorem.

Map[implies[subclass[image[CAP, cart[x, x]], x], #] &, 
      SubstTest[subclass, composite[t, t], t, 
        t -> composite[CAP, id[cart[V, x]], inverse[FIRST]]]]

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

The following lemma can be used to generalize this result slightly.

SubstTest[implies, TRANSITIVE[t], 
        TRANSITIVE[
          composite[t, id[x]]], 
{t -> 
            composite[CAP, id[cart[V, y]], inverse[FIRST]]}] // 
      Reverse

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

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> subclass[image[CAP, cart[y, y]], y], 
            p2 -> TRANSITIVE[
                composite[CAP, id[cart[V, y]], 
                  inverse[FIRST]]], 
p3 -> 
              TRANSITIVE[composite[CAP, id[cart[x, y]], inverse[FIRST]]]}]] // 
      Reverse

or[not[subclass[image[CAP, cart[y_, y_]], y_]], 
        TRANSITIVE[composite[CAP, id[cart[x_, y_]], inverse[FIRST]]]] := 
      True

Transitive laws for two important special cases are immediate corollaries.

SubstTest[implies, subclass[image[CAP, cart[y, y]], y], 
        TRANSITIVE[composite[CAP, id[cart[x, y]], inverse[FIRST]]], 
        y -> range[CART]] // Reverse

TRANSITIVE[composite[CAP, id[cart[x_, range[CART]]], inverse[FIRST]]] := 
      True

Corollary.

SubstTest[implies, subclass[image[CAP, cart[y, y]], y], 
        TRANSITIVE[composite[CAP, id[cart[x, y]], inverse[FIRST]]], 
        y -> image[CART, Id]] // Reverse

TRANSITIVE[
        composite[CAP, id[cart[x_, image[CART, Id]]], inverse[FIRST]]] := 
      True

reflexivity of erasure relations

A general condition for reflexivity can be derived:

REFLEXIVE[composite[CAP, id[x], inverse[FIRST]]] // 
      AssertTest

REFLEXIVE[composite[CAP, id[x_], inverse[FIRST]]] := 
      and[subclass[domain[x], fix[composite[inverse[S], x]]], 
        subclass[image[CAP, x], fix[composite[inverse[S], x]]]]

Note that the reflexive property fails for the two main types of erasure under consideration if one does not restrict the erasure process to relations:

REFLEXIVE[
      composite[CAP, id[cart[V, range[CART]]], inverse[FIRST]]]

REFLEXIVE[
      composite[CAP, id[cart[V, image[CART, Id]]], 
        inverse[FIRST]]]

One can fix this up by considering the restriction of these erasure relations to the class P[cart[V, V]] of relations.

REFLEXIVE[
      composite[CAP, id[cart[P[cart[V, V]], range[CART]]], 
        inverse[FIRST]]]

REFLEXIVE[
      composite[CAP, id[cart[P[cart[V, V]], image[CART, Id]]], 
        inverse[FIRST]]]

two examples of interest

Theorem.  Horizontal and vertical erasure is a partial ordering on the class of relations.

SubstTest[and, REFLEXIVE[t], TRANSITIVE[t], 
      subclass[intersection[t, inverse[t]], Id], 
t -> 
        composite[CAP, id[cart[P[cart[V, V]], range[CART]]], 
          inverse[FIRST]]]

PARTIALORDER[
        composite[CAP, id[cart[P[cart[V, V]], range[CART]]], 
          inverse[FIRST]]] := True

Theorem.   Symmetric erasure defines a partial ordering on the class PO of partial orders.

SubstTest[and, REFLEXIVE[t], TRANSITIVE[t], 
      subclass[intersection[t, inverse[t]], Id], 
t -> 
        composite[CAP, id[cart[PO, image[CART, Id]]], 
          inverse[FIRST]]]

PARTIALORDER[
        composite[CAP, id[cart[PO, image[CART, Id]]], inverse[FIRST]]] := 
      True

Note that the fixed point set of this ordering is indeed the class PO.

fix[
      composite[CAP, id[cart[PO, image[CART, Id]]], 
        inverse[FIRST]]]