the class RS[x] of small restrictions, part 3

Johan G. F. Belinfante
revised 2004 August 10

SetDirectory["i:"]; << goedel60.10a;  <<  tools.m;

summary

In this third notebook dealing with the theory of RS[x], a study is made of the functon  VERTSECT[RESTRICT] = lambda[x, RS[x]].  This function allows one to formulate variable-free equations that capture the facts about  RS[x] for the case that  x  is a set.  An additional bonus of this endeavor is the discovery of a cornucopia of new facts about the relation RESTRICT which had up to now only been studied cursorily.

the connection between  RESTRICT and RS[x]

The relation RESTRICT is the class of all ordered pairs pair[x,y]  such that y is a restriction of x.

class[pair[x, y], 
      exists[z, and[subclass[z, Id], equal[y, composite[x, z]]]]]

The relation RESTRICT was actually defined by the following membership rule, which will shortly be replaced.

member[pair[x, y], RESTRICT]

The key result needed to connect this relation RESTRICT with RS[x] is this formula:

ImageComp[COMPOSE, LEFT[x], P[Id]] // Reverse

image[COMPOSE, cart[singleton[x_], P[Id]]] := 
      intersection[image[V, singleton[x]], RS[x]]

new membership rule for RESTRICT

The key result found in the preceding section causes the membership rule that defined the relation RESTRICT to be transformed:

member[x, RESTRICT]

For ordered pairs, this formula becomes rather ugly, so we temporarily remove the old rule, derive a separate rule for membership of pairs, and then restore the above rule.

member[x_, RESTRICT] =.

Lemma.

SubstTest[member, pair[x, y], composite[Id, z], z -> RESTRICT] // 
      Reverse

and[member[x_, V], member[y_, V], member[pair[x_, y_], RESTRICT]] := 
      member[pair[x, y], RESTRICT]

This is the new membership rule for pairs:

SubstTest[member, y, image[z, singleton[x]], z -> RESTRICT] // 
      Reverse

member[pair[x_, y_], RESTRICT] := 
      and[equal[y, composite[x, id[domain[y]]]], member[x, V], 
        member[y, V]]

The following tricky maneuver restores the replacement for the general membership rule:

(member[x, 
            composite[rotate[rotate[w]], id[cart[V, P[Id]]], 
              inverse[FIRST]]] // AssertTest) /. 
      w -> rotate[COMPOSE]

member[x_, RESTRICT] := 
      and[equal[composite[first[x], id[domain[second[x]]]], second[x]], 
        member[first[x], V]]

normalization rule

Subsequent derivations are simplified if one normalizes RESTRICT.

RESTRICT // VSNormality // Reverse

composite[
        intersection[inverse[S], 
          UB[union[E, 
              composite[inverse[IMAGE[FIRST]], complement[E], FIRST]]]], 
        IMAGE[id[cart[V, V]]]] := RESTRICT

a partial order related to RESTRICT

The relation  RESTRICT  is idempotent, antisymmetric, and transitive.  It fails to be a partial order because it lacks the reflexive property.

{REFLEXIVE[x], ANTISYMMETRIC[x], TRANSITIVE[x], idempotent[x]} /. 
      x -> RESTRICT

The breakdown of the reflexive law stems from the fact that its domain is larger than its fixed point set.

{domain[RESTRICT], range[RESTRICT], fix[RESTRICT]}

It will now be shown using AssertTest that the restriction of RESTRICT to relations is a partial order. Sequestering RESTRICT from the action of AssertTest speeds this up.

(REFLEXIVE[composite[x, id[P[cart[V, V]]]]] // AssertTest) /. 
      x -> RESTRICT

REFLEXIVE[composite[RESTRICT, id[P[cart[V, V]]]]] := True

(TRANSITIVE[composite[x, id[P[cart[V, V]]]]] // AssertTest) /. 
      x -> RESTRICT

TRANSITIVE[composite[RESTRICT, id[P[cart[V, V]]]]] := True

Combining these lemmas yields the stated result.

SubstTest[and, REFLEXIVE[x], ANTISYMMETRIC[x], TRANSITIVE[x], 
        x -> composite[RESTRICT, id[P[cart[V, V]]]]] // 
      Reverse

PARTIALORDER[composite[RESTRICT, id[P[cart[V, V]]]]] := True

a formula for APPLY[VERTSECT[RESTRICT], x]

The relation RESTRICT is known to be thin:

thin[RESTRICT]

On account of this, the image under RESTRICT of any set is a set:

Map[implies[member[x, y], #] &, 
      SubstTest[implies, and[thin[z], member[x, V]], member[image[z, x], V], 
        z -> RESTRICT]]

or[member[image[COMPOSE, cart[x_, P[Id]]], V], not[member[x_, y_]]] := 
      True

In particular, all its vertical sections are sets:

member[image[RESTRICT, singleton[x]], V]

The following consequence of this will be used to simplify a formula for the application of the function VERTSECT[RESTRICT].

equal[
      union[complement[image[V, singleton[x]]], 
        complement[image[V, singleton[RS[x]]]]], 
      complement[image[V, singleton[x]]]]

union[complement[image[V, singleton[x_]]], 
        complement[image[V, singleton[RS[x_]]]]] := 
      complement[image[V, singleton[x]]]

One now obtains the following clean formula for the application of the function VERTSECT[RESTRICT] to any argument.

SubstTest[A, image[z, singleton[x]], z -> VERTSECT[RESTRICT]] // 
      Reverse

APPLY[VERTSECT[RESTRICT], x_] := 
      union[complement[image[V, singleton[x]]], RS[x]]

Note that for sets, this formula simplifies further:

APPLY[VERTSECT[RESTRICT], setpart[x]]

In other words, one can regard VERTSECT[RESTRICT] as the function which takes any set x to RS[x].  This can also be established as follows:

lambda[x, RS[x]]

Since  RS[x]  is a set whenever  x  is a set, the function  lambda[x, RS[x]] = VERTSECT[RESTRICT]  is total:

domain[VERTSECT[RESTRICT]]

This is equivalent to the statement that the relation RESTRICT is thin.

variable-free formulation of a characterization of functions

One can use the function VERTSECT[RESTRICT] to derive variable-free equations that capture that part of the theory of the class RS[x] that applies to the special case that  x  is a set.  For example, the formula for restrictions of a function can be written as follows:

composite[VERTSECT[RESTRICT], FUNPART] // VSNormality

composite[VERTSECT[RESTRICT], FUNPART] := 
      composite[POWER, FUNPART]

The theorem that RS[x] = P[x] characterizes functions can be written without variables as follows:

fix[composite[inverse[POWER], VERTSECT[RESTRICT]]] // 
      Normality

fix[composite[inverse[POWER], VERTSECT[RESTRICT]]] := FUNS

Corollary 1.

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
      equal[u, composite[v, id[domain[u]]]], 
{u -> 
          intersection[POWER, VERTSECT[RESTRICT]], 
        v -> POWER}]

intersection[POWER, VERTSECT[RESTRICT]] := 
      composite[POWER, id[FUNS]]

Corollary 2.

SubstTest[range, 
        intersection[u, v], {u -> POWER, v -> VERTSECT[RESTRICT]}] // 
      Reverse

fix[composite[POWER, inverse[VERTSECT[RESTRICT]]]] := 
      image[POWER, FUNS]

variable-free reformulations of some other facts about RS[x]

The variable-free counterpart of the equation  U[RS[x]] = thinpart[x] is already known:

composite[BIGCUP, VERTSECT[RESTRICT]]

The variable-free version of the formula RS[composite[Id,x]] = RS[x] can be derived as follows:

Map[composite[VERTSECT[#], SINGLETON] &, 
      Assoc[RESTRICT, IMAGE[id[cart[V, V]]], inverse[E]]]

A less clever derivation of this result is possible, using a standard technique using  VSNormality and symdif.  This requires two steps:

symdif[composite[VERTSECT[RESTRICT], IMAGE[id[cart[V, V]]]], 
        VERTSECT[RESTRICT]] // VSNormality

% /. Equal -> SetDelayed

SubstTest[equal, 0, 
      symdif[u, 
        v], {u -> composite[VERTSECT[RESTRICT], IMAGE[id[cart[V, V]]]], 
        v -> VERTSECT[RESTRICT]}]

composite[VERTSECT[RESTRICT], IMAGE[id[cart[V, V]]]] := 
      VERTSECT[RESTRICT]

reification rule for RS[x]

Reification provides a powerful tool for deriving variable-free counterparts of rewrite rules with variables.  A useful reification rule for RS[x] is obtained as follows:

SubstTest[reify, x, image[IMAGE[cross[Id, f[x]]], y], 
      y -> P[Id]]

reify[x_, RS[y_]] := 
      composite[IMAGE[composite[SWAP, RIF, cross[reify[x, y], Id]]], CART, 
        id[cart[V, P[Id]]], inverse[FIRST], SINGLETON]

In particular, one has

reify[x, RS[x]]

variable-free results obtained using reification

In this section some examples are presented to illustrate the use of reification to recast results about  RS[x] as equatons without variables.  As a first example, reification is used to eliminate the variable x from the rewrite rule for U[RS[x]].

SubstTest[reify, x, U[f[x]], f -> RS] // Reverse

This particular equation can also be independently derived from existing facts about RESTRICT as follows:

Assoc[inverse[E], inverse[S], RESTRICT] // Reverse

composite[inverse[E], RESTRICT] := 
      composite[inverse[E], IMAGE[id[cart[V, V]]]]

The same technique can be used to derive other new properties of  RESTRICT, for instance,

Assoc[complement[inverse[E]], S, RESTRICT] // Reverse

This result corresponds to the fact that A[RS[x]] = 0, as can be seen from the following alternate derivation, using reification:

Map[composite[Id, complement[#]] &, 
        SubstTest[reify, x, A[f[x]], f -> RS]] // Reverse

composite[complement[inverse[E]], RESTRICT] := cart[V, V]

Aclosure and Uclosure

The facts that RS[x] is closed under arbitrary intersections and under arbitrary unions have simple variable-free formulations:

Map[VERTSECT, SubstTest[reify, x, Aclosure[f[x]], f -> RS]] // 
      Reverse

composite[ACLOSURE, VERTSECT[RESTRICT]] := 
      VERTSECT[RESTRICT]

Map[VERTSECT, SubstTest[reify, x, Uclosure[f[x]], f -> RS]] // 
      Reverse

composite[UCLOSURE, VERTSECT[RESTRICT]] := 
      VERTSECT[RESTRICT]

ONEONE property of a restriction of VERTSECT[RESTRICT]

One can see that the function VERTSECT[RESTRICT] fails to be one-to-one because RS[x] for example is equal to RS[composite[Id,x]].  It will be shown that the restriction of the function VERTSECT[RESTRICT] to the class P[cart[V, V]] of all relations is one-to-one.  The one-to-one property will be derived by analogy with the following:

SubstTest[implies, equal[u, v], 
      equal[U[u], U[v]], {u -> RS[x], v -> RS[y]}]

or[equal[thinpart[x_], thinpart[y_]], not[equal[RS[x_], RS[y_]]]] := 
      True

Lemma.

composite[inverse[VERTSECT[RESTRICT]], inverse[BIGCUP]] // 
      DoubleInverse

composite[inverse[VERTSECT[RESTRICT]], inverse[BIGCUP]] := 
      inverse[IMAGE[id[cart[V, V]]]]

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], 
{u -> Id, 
        v -> composite[inverse[BIGCUP], BIGCUP], 
        w -> inverse[
            cross[VERTSECT[RESTRICT], VERTSECT[RESTRICT]]]}]

% /. Equal -> SetDelayed

For the reverse inclusion one needs the following lemma:

composite[inverse[IMAGE[id[cart[V, V]]]], inverse[VERTSECT[RESTRICT]]] // 
      DoubleInverse

composite[inverse[IMAGE[id[cart[V, V]]]], inverse[VERTSECT[RESTRICT]]] := 
      inverse[VERTSECT[RESTRICT]]

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], 
{u -> Id, 
        v -> composite[inverse[VERTSECT[RESTRICT]], VERTSECT[RESTRICT]], 
        w -> 
          inverse[cross[IMAGE[id[cart[V, V]]], 
              IMAGE[id[cart[V, V]]]]]}]

% /. Equal -> SetDelayed

Putting these facts together yields:

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> composite[inverse[IMAGE[id[cart[V, V]]]], 
            IMAGE[id[cart[V, V]]]], 
        v -> composite[inverse[VERTSECT[RESTRICT]], 
            VERTSECT[RESTRICT]]}]

composite[inverse[VERTSECT[RESTRICT]], VERTSECT[RESTRICT]] := 
      composite[inverse[IMAGE[id[cart[V, V]]]], 
        IMAGE[id[cart[V, V]]]]

Corollary.

SubstTest[subclass, composite[x, inverse[x]], 
        id[y], {x -> 
            composite[id[P[cart[V, V]]], inverse[VERTSECT[RESTRICT]]], 
          y -> P[cart[V, V]]}] // Reverse

FUNCTION[composite[id[P[cart[V, V]]], inverse[VERTSECT[RESTRICT]]]] := 
      True

a formula for image[inverse[S], RS[x]]

Lemma.

Assoc[x, id[domain[VERTSECT[x]]], id[y]]

composite[x_, id[intersection[y_, domain[VERTSECT[x_]]]]] := 
      composite[thinpart[x], id[y]]

If  y  is a subset of thinpart[x], then y is contained in the restriction of thinpart[x] to domain[y]. This is the idea behind the following.

implies[member[domain[y], V], 
        member[composite[thinpart[x], id[domain[y]]], RS[x]]] // 
      NotNotTest

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

Map[equal[V, class[y, #]] &, 
      Map[not, SubstTest[and, implies[and[p1, p2], p3], implies[p1, p4], 
            implies[and[p1, p2, p3, p4], p5], implies[and[p5, p6], p7], 
            implies[and[p3, p7], p8], 
not[
              implies[and[p1, p2, p6], p8]], {p1 -> 
                member[y, P[thinpart[x]]], 
              p2 -> equal[w, composite[thinpart[x], id[domain[y]]]], 
              p3 -> subclass[y, w], p4 -> member[domain[y], V], 
              p5 -> member[w, RS[x]], p6 -> equal[z, RS[x]], 
              p7 -> member[w, z], 
              p8 -> member[y, image[inverse[S], z]]}]] /. {w -> 
            composite[thinpart[x], id[domain[y]]], 
          z -> RS[x]}]

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

The reverse inclusion also holds, so one can sharpen this to an equation:

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> P[thinpart[x]], 
        v -> image[inverse[S], RS[x]]}]

image[inverse[S], RS[x_]] := P[thinpart[x]]

The variable-free equation corresponding to this is:

Map[composite[VERTSECT[#], SINGLETON] &, 
      Assoc[inverse[S], RESTRICT, inverse[E]]]

composite[IMAGE[inverse[S]], VERTSECT[RESTRICT]] := 
      composite[POWER, IMAGE[id[cart[V, V]]]]

some new formulas for RESTRICT

The following old formula for RESTRICT is useful for deriving various properties of this relation

composite[COMPOSE, id[cart[V, P[Id]]], inverse[FIRST]]

For example, one can use it to derive the following property of RESTRICT:

Assoc[IMAGE[SECOND], COMPOSE, 
      composite[id[cart[V, P[Id]]], inverse[FIRST]]]

This equation can also be derived a different way using this famous connection between the functions  IMG  and  CART:

composite[IMAGE[rotate[Id]], CART]

The following alternate derivation is based on this idea:

Assoc[IMAGE[rotate[Id]], CART, inverse[FIRST]]

composite[IMAGE[SECOND], RESTRICT] := 
      composite[IMG, inverse[FIRST]]

A lemma is needed to get a corresponding result with IMAGE[FIRST] in place of IMAGE[SECOND].

composite[IMG, id[cart[P[Id], V]], inverse[SECOND]] // 
      VSNormality

composite[IMG, id[cart[P[Id], V]], inverse[SECOND]] := 
      inverse[S]

Assoc[IMAGE[FIRST], COMPOSE, 
      composite[id[cart[V, P[Id]]], inverse[FIRST]]]

composite[IMAGE[FIRST], RESTRICT] := 
      composite[inverse[S], IMAGE[FIRST]]

interpreting the formulas

In addition to finding variable-free equations corresponding to properties of RS[x], one can also try to do the reverse, finding properties of RS[x] that correspond to identities involving RESTRICT.  This is less automatic because the variable-free equations only yield results valid when  x  is a set.  One needs to go further to obtain completely general results.  Nonetheless, the variable-free requations are useful for suggesting what one must do.  For example, the interpretation of the IMAGE[SECOND] formula found in the preceding section is that the class of all ranges of restrictions of  x is the range of the function IMAGE[x].  To get a general result of this sort, one needs to use a method that does not require  x  to be a set.  In this case, the following works:

ImageComp[IMAGE[SECOND], IMAGE[cross[Id, x]], P[Id]] // 
      Reverse

image[IMAGE[SECOND], RS[x_]] := range[IMAGE[x]]

The interpretation of the IMAGE[FIRST] formula is that the class of all domains of restrictions of  x is the power class of the domain of the thinpart of  x.  This fact is established as follows:

Map[equal[P[domain[thinpart[x]]], image[#, P[Id]]] &, 
      composite[IMAGE[FIRST], IMAGE[cross[Id, x]]] // VSNormality]

image[IMAGE[FIRST], RS[x_]] := 
      P[intersection[domain[x], domain[VERTSECT[x]]]]

Recall that the domain of the thin part of  x  is

domain[thinpart[x]]

When  x  is a function, this formula reduces to

image[IMAGE[FIRST], P[funpart[x]]]

A similar result holds with the funpart wrapper replaced with thinpart or setpart, but it is currently not known whether the wrapper can be removed altogether.  The following inclusion holds, but it is currently not known whether the reverse inclusion holds for arbitrary classes:

subclass[image[IMAGE[FIRST], P[x]], P[domain[x]]]