the class RS[x] of small restrictions, part 1.

Johan G. F. Belinfante
2004 August 7

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

summary

This notebook introduces the class  RS[x] of all small restrictions of  a class  x.  A restriction of  x  is any class of the form  composite[x, id[y]].  A restriction is small if it is a set.  Several different formulas will be obtained for the class of all small restrictions, any one of which could be used to define  RS[x]  for theorem proving using Otter.  In the GOEDEL program a membership rule is used to define the class constructor RS[x], and various forms of normality tests are used to obtain equations for  RS[x].   Several properties of this new constructor will be derived, and some examples given.

eliminating an existential quantifier

There are several candidates for the membership rule used to define the class of small restrictions.  To obtain a rule that is not wrapped with class, one needs to eliminate all quantifiers.  A natural definition for this class uses an existential quantifier:  x  is a restriction of  y  if there exists a set  z  such that  x = composite[y,id[z]].  One can use assert to eliminate the existential quantifier::

assert[
      and[member[x, V], exists[z, equal[x, composite[y, id[z]]]]]]

This definition can be simplied.  In the first place, one would prefer an equation in place of the inclusion  subclass[composite[y, id[domain[x]]], x].   The equation that is contemplated can be studied using AssertTest:

equal[x, composite[y, id[domain[x]]]] // AssertTest

The condition subclass[x, cart[domain[x], V] can be simplified.  To do so, the following lemma is useful.

SubstTest[implies, and[equal[x, y], subclass[y, cart[domain[y], V]]], 
      subclass[x, cart[domain[x], V]], y -> composite[Id, x]]

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

This can be restated as a logical equivalence:

equiv[subclass[x, cart[domain[x], V]], 
      subclass[x, cart[V, V]]]

On the basis of this observation, one is justified in adding the following rewrite rule:

subclass[x_, cart[domain[x_], V]] := subclass[x, cart[V, V]]

With this rule in place, the AssertTest performed above for the equation under consideration can be repeated, and then turned around to be made into a rewrite rule:

equal[x, composite[y, id[domain[x]]]] // AssertTest // 
      Reverse

and[subclass[x_, y_], subclass[x_, cart[V, V]], 
        subclass[composite[y_, id[domain[x_]]], x_]] := 
      equal[x, composite[y, id[domain[x]]]]

With these simplifications in place, the quantifier elimination yields a simpler result:

and[member[x, V], 
      assert[exists[z, equal[x, composite[y, id[z]]]]]]

definition of the class constructor RS[x]

Based on the work done in the preceding section, the following unwrapped membership rule will be used to define the class constructor RS[x].

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

As an example, we note that  RS[x] is never empty because  0  is always a restriction:

member[0, RS[x]]

As a corollary, one has:

SubstTest[and, member[0, w], equal[0, w], w -> RS[x]]

equal[0, RS[x_]] := False

basic normalization result

Normalization is used to prevent the class constructor  RS[x]  from being rewritten when class is applied.  The idea is to add rewrite rules that will generall transform expressions produced by such applications back to  RS[x].  The simplest result of this type is:

RS[x] // Normality // Reverse

intersection[invar[composite[id[x_], inverse[FIRST], FIRST]], 
        P[thinpart[x_]]] := RS[x]

As an elementary application of normalization, one can now deduce that the restrictions of  x  and of its relational part composite[Id, x] are the same, as one would expect.

RS[composite[Id, x]] // Normality

RS[composite[Id, x_]] := RS[x]

some extreme cases

Another simple application of normality is to derive the basic fact that for both the empty set and the universal class, the only small restriction is the empty set.

RS[0] // Normality

RS[0] := singleton[0]

RS[V] // Normality

RS[V] := singleton[0]

There are other classes in between these extremes for which  RS[x] is nontrivial, for example,

RS[Id] // Normality

RS[Id] := P[Id]

It is clear from these examples that the constructor  RS[x]  cannot be either antitone or monotone.

Uclosure and Aclosure results

A closer examination of the expression occurring in the basic normalization rule leads to some unexpected discoveries.  Observe that the relation that appears inside the invar expression in this normalization rule has the remarkable property of being idempotent, a fact that will be exploited shortly.

idempotent[composite[id[x], inverse[FIRST], FIRST]]

In general, the condition for invariance involves only an inclusion:

member[w, invar[z]]

Replacing the inclusion by equality yields a fixed point set:

class[w, equal[image[z, w], w]]

Using normality to study this quantity for the case of the idempotent relation  z = composite[id[x],inverse[FIRST],FIRST]  reveals the not so obvious fact that RS[x]  is the fixed-point set for an idempotent function.

fix[IMAGE[composite[id[x], inverse[FIRST], FIRST]]] // 
      Normality

fix[composite[IMAGE[composite[id[x_], inverse[FIRST]]], IMAGE[FIRST]]] := 
      RS[x]

An immediate corollary of this formula is that the union of any set of restrictions is again a restriction, that is, RS[x] is closed under arbitrary unions.

SubstTest[Uclosure, fix[IMAGE[z]], 
      z -> composite[id[x], inverse[FIRST], FIRST]]

Uclosure[RS[x_]] := RS[x]

A similar result holds for intersections, but one needs to use a different argument.  The normalization rule again enters into this derivation.

SubstTest[implies, and[equal[Aclosure[u], u], equal[Aclosure[v], v]], 
      equal[Aclosure[intersection[u, v]], 
        intersection[u, v]], 
{u -> 
          invar[composite[id[x], inverse[FIRST], FIRST]], 
        v -> P[thinpart[x]]}]

Aclosure[RS[x_]] := RS[x]

further consequences of idempotence

The idempotence of any relation  z  implies that the corresponding function  IMAGE[z]  is also idempotent.  In the present case, this fact is rewritten in an obscure form, but that is of no particular concern.

SubstTest[implies, idempotent[z], idempotent[IMAGE[z]], 
      z -> composite[id[x], inverse[FIRST], FIRST]]

Since this is an equation, it can be saved either as a fact, or as a rewrite rule that transforms one side to the other.  The latter will be adopted here:

composite[IMAGE[composite[id[x_], inverse[FIRST]]], IMAGE[FIRST], 
        IMAGE[id[cart[domain[x_], V]]]] := 
      composite[IMAGE[composite[id[x], inverse[FIRST]]], 
        IMAGE[FIRST]]

The important thing to observe here is that the fixed point set and the range of any idempotent function are equal, from which one can derive a new formula for  RS[x].

SubstTest[implies, and[idempotent[w], FUNCTION[w]], 
      equal[range[w], fix[w]], 
      w -> composite[IMAGE[composite[id[x], inverse[FIRST]]], 
          IMAGE[FIRST]]]

This equation is not saved as a fact, but as a rule transforming a fairly complex expression to a compact one.  It should be noted by the way that the IMAGE function appearing in this new rewrite rule is not the idempotent function considered earlier, but rather another function closely related to it, but which lacks the idempotence property.

range[IMAGE[composite[id[x_], inverse[FIRST]]]] := RS[x]

The fixed point set of an IMAGE[z] function can be written as the intersection of invar[z] and subvar[z].  This yields the following formula which is similar to the one derived in the preceding section, but simpler in that thinpart[x] is replaced with composite[Id, x].

SubstTest[intersection, subvar[z], invar[z], 
      z -> composite[id[x], inverse[FIRST], FIRST]]

intersection[invar[composite[id[x_], inverse[FIRST], FIRST]], 
        P[composite[Id, x_]]] := RS[x]

trv result

Any idempotent relation is transitive, so in particular:

SubstTest[implies, idempotent[y], equal[trv[y], y], 
      y -> composite[id[x], inverse[FIRST], FIRST]]

TRANSITIVE[composite[id[x_], inverse[FIRST], FIRST]] := True

An idempotent relation is its own transitive closure:

equal[trv[composite[id[x], inverse[FIRST], FIRST]], 
      composite[id[x], inverse[FIRST], FIRST]]

trv[composite[id[x_], inverse[FIRST], FIRST]] := 
      composite[id[x], inverse[FIRST], FIRST]

This transitive closure result is mainly of interest due to the following rewrite rule:

U[invar[z]]

For the special case of  z = composite[id[x], inverse[FIRST], FIRST], one now gets the following result which no longer involves trv explicitly.

U[invar[composite[id[x],  inverse[FIRST],  FIRST]]]

class results

The class RS[x] can be characterized using class in various ways, some of which lead to new formulas for  RS[x].  This first one works fine with the existing rules:

class[w, equal[w, composite[x, id[domain[w]]]]]

The following alternate expression does not immediately simplify to  RS[x], but instead yields a messy result that one must come to grips with:

class[w, exists[y, equal[w, composite[x, id[y]]]]]

Rather than looking at the complete expression, it is useful to focus on the fix term that occurs in it.  When one studies this term using Normality, another complicated result is obtained, but miraculously this result simplifies dramatically when one intersects it with P[composite[Id,x]]:

Map[intersection[#, P[composite[Id, x]]] &, 
      fix[composite[S, IMAGE[composite[id[x], inverse[FIRST]]], S, 
            IMAGE[FIRST]]] // Normality]

intersection[
        fix[composite[S, IMAGE[composite[id[x_], inverse[FIRST]]], S, 
            IMAGE[FIRST]]], P[composite[Id, x_]]] := RS[x]

Now everything works fine for this class expression:

class[w, exists[y, equal[w, composite[x, id[y]]]]]

removing and replacing an old rewrite rule

As a variation on the class expression considered in the preceding section, one can try replacting the piece composite[x, id[y]] in it with the less explicit term composite[x, z] at the same time adding the condition that z is a subset of Id.

class[z, exists[y, equal[z, id[y]]]]

This idea is explored below, yielding yet another useful characterization of  RS[x], but before getting started, one needs to be aware that the GOEDEL program already has a rewrite rule that must be removed.  It will be shortly be replaced with a simpler new one, but for now it is just best to get it out of the way.

image[IMAGE[cross[Id, x_]], P[Id]] =.

With the old rule removed, one is ready to study the proposed characterization of the class of small restrictions:

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

The removed rule will now be replaced with the following simpler one:

Map[range, 
      composite[IMAGE[cross[Id, x]], IMAGE[id[Id]]] // 
        RelnNormality]

image[IMAGE[cross[Id, x_]], P[Id]] := RS[x]

For the record we note that the proposed class expression does reduce to RS[x], as expected.

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

thinpart

The replacement rewrite rule derived in the last section has many interesting applications.  This one is basic:

SubstTest[U, image[IMAGE[z], P[Id]], z -> cross[Id, x]]

U[RS[x_]] := thinpart[x]

Using the formula that expresses  RS[x]  as the range of an IMAGE function, one deduces this corollary:

SubstTest[U, range[IMAGE[w]], w -> composite[id[x], inverse[FIRST]]] // 
      Reverse

U[range[VERTSECT[composite[id[x_], inverse[FIRST]]]]] := 
      thinpart[x]

Other formulas for  RS[x]  yield other such corollaries.  They all say more or less the same thing, but in different ways.

SubstTest[U, 
        intersection[u, 
          P[v]], {u -> invar[composite[id[x], inverse[FIRST], FIRST]], 
          v -> thinpart[x]}] // Reverse

core[invar[composite[id[x_], inverse[FIRST], FIRST]], thinpart[x_]] := 
      thinpart[x]

SubstTest[U, 
        intersection[u, 
          P[v]], {u -> invar[composite[id[x], inverse[FIRST], FIRST]], 
          v -> composite[Id, x]}] // Reverse

core[invar[composite[id[x_], inverse[FIRST], FIRST]], 
        composite[Id, x_]] := thinpart[x]

An important corollary of the basic result in this section is that the class of small restrictions RS[x]  is a subclass of the power class P[x].

subclass[RS[x], P[x]]

sethood rule

The formula for  U[RS[x]] permits one to obtain a simple criterion for the class  RS[x] to be a set.

SubstTest[member, U[w], V,  w -> RS[x]] // Reverse

member[RS[x_], V] := member[thinpart[x], V]

In particular, when  x  is a set, so is RS[x].

implies[member[x, V], member[RS[x], V]]

It follows that there is a total function that takes  x  to  RS[x].  This function is VERTSECT[RESTRICT]; it will be studied in a later notebook.

characterizing when 0 is the only restriction of x

An interesting application of the formula for U[RS[x]]  is to identify those classes  x  for which  0  is the only small restriction.  A temporary rule will be introduced to simplify the result.

equal[0, domain[thinpart[x]]] // AssertTest // Reverse

equal[0, intersection[domain[x_], domain[VERTSECT[x_]]]] := 
      equal[0, domain[thinpart[x]]]

The main result is this:

SubstTest[equal, 0, U[w], w -> RS[x]] // Reverse

subclass[RS[x_], singleton[0]] := 
      equal[0, domain[thinpart[x]]]

One can replace inclusion with equality.

equal[singleton[0], RS[x]] // AssertTest

equal[RS[x_], singleton[0]] := equal[0, domain[thinpart[x]]]