intersection[RFX,TRV]

Johan G. F. Belinfante
2004 December 18

SetDirectory["i:"]; << goedel64.17b; << tools.m

summary

Reflexive transitive relations, also known as quasi-orders, satisfy some properties analogous to those of equivalence relations.  In this notebook, variable-free formulations of facts about the class intersection[RFX,TRV] of small reflexive symmetric relations are derived, culminating in a formula for a canonical factorization of such relations.

reflexive core of a transitive relation

If  x  is transitive, so is its reflexive core.

SubstTest[implies, TRANSITIVE[x], TRANSITIVE[restrict[x, y, y]], 
      y -> fix[x]]

or[not[TRANSITIVE[x_]], TRANSITIVE[rfx[x_]]] := True

The class TRV is invariant under CORE[RFX].

Map[equal[0, composite[Id, complement[#]]] &, 
        SubstTest[class, pair[x, z], 
          implies[member[z, image[u, singleton[setpart[x]]]], 
            member[z, v]], {u -> 
              composite[HULL[TRV], IMAGE[id[cart[V, V]]]], 
            v -> image[inverse[CORE[RFX]], TRV]}]] // Reverse

% /. Equal -> SetDelayed

The image is also contained in RFX.

Map[subclass[#, RFX] &, ImageComp[id[RFX], CORE[RFX], TRV]]

% /. Equal -> SetDelayed

The reverse inclusion also holds:

SubstTest[implies, subclass[u, v], 
      subclass[image[u, w], image[v, w]], {u -> id[RFX], 
        v -> CORE[RFX], w -> TRV}]

% /. Equal -> SetDelayed

The following equation follows:

equal[image[CORE[RFX], TRV], intersection[RFX, TRV]] // 
      AssertTest

image[CORE[RFX], TRV] := intersection[RFX, TRV]

an antitone property of vertical sections

The truth of the following statement is currently recognized by the GOEDEL program.  It says that the vertical sections of a transitive relation satisfy an antitone property with respect to inclusions: if  u  is related to  v  by a transitive relation  x, then the vertical section of  v  is contained in that of  u.

or[not[member[pair[u, v], x]], not[TRANSITIVE[x]], 
      subclass[image[x, singleton[v]], image[x, singleton[u]]]]

A version of this fact which eliminates the variables  u  and  v  is readily derived in the case that  x  is thin:

Map[subclass[x, #] &, 
      composite[inverse[VERTSECT[x]], inverse[S], VERTSECT[x]] // 
        RelnNormality]

subclass[x_, 
        composite[inverse[VERTSECT[x_]], inverse[S], VERTSECT[x_]]] := 
      and[equal[V, domain[VERTSECT[x]]], TRANSITIVE[x]]

The following corollary requires nothing further:

subclass[x, 
      composite[id[fix[x]], inverse[VERTSECT[x]], inverse[S], VERTSECT[x], 
        id[fix[x]]]]

It will be shown below that this inclusion can be replaced with an equation.

a factorization result

Recall that  composite[inverse[funpart[x]], inverse[S], funpart[x]]  is both reflexive and transitive.  Variable-free restatements of these facts can be obtained as follows.  For the reflexive property, one obtains:

Map[equal[V, #] &, 
        SubstTest[class, x, 
          subclass[image[u, singleton[setpart[x]]], 
            v], {u -> composite[COMPOSE, 
                intersection[composite[inverse[FIRST], INVERSE], 
                  composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
                FUNPART], v -> RFX}]] // Reverse

% /. Equal -> SetDelayed

A similar result holds for the transitive property:

Map[equal[V, #] &, 
        SubstTest[class, x, 
          subclass[image[u, singleton[setpart[x]]], 
            v], {u -> composite[COMPOSE, 
                intersection[composite[inverse[FIRST], INVERSE], 
                  composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
                FUNPART], v -> TRV}]] // Reverse

% /. Equal -> SetDelayed

These two results will now be solved to derive an lower bound for  intersection[RFX,TRV].  Note that the following is a function:

abstract[x, 
      image[COMPOSE, 
        composite[IMAGE[cross[Id, inverse[S]]], id[x], INVERSE]]]

composite[COMPOSE, 
        intersection[composite[inverse[FIRST], INVERSE], 
          composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]]] // 
      FUNCTION

Consequently, one has:

SubstTest[composite, funpart[x], 
      inverse[funpart[x]], 
x -> 
        composite[COMPOSE, 
          intersection[composite[inverse[FIRST], INVERSE], 
            composite[inverse[SECOND], 
              IMAGE[cross[Id, inverse[S]]]]]]]

% /. Equal -> SetDelayed

Corollary:

ImageComp[
        composite[COMPOSE, 
          intersection[composite[inverse[FIRST], INVERSE], 
            composite[inverse[SECOND], 
              IMAGE[cross[Id, inverse[S]]]]]], 
inverse[
          composite[COMPOSE, 
            intersection[composite[inverse[FIRST], INVERSE], 
              composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]]]], 
        x] // Reverse

This is made into a temporary rewrite rule:

image[COMPOSE, 
        composite[IMAGE[cross[Id, inverse[S]]], 
          id[fix[composite[INVERSE, inverse[image[inverse[COMPOSE], x_]], 
                IMAGE[cross[Id, inverse[S]]]]]], INVERSE]] := 
      intersection[x, 
        image[COMPOSE, 
          composite[IMAGE[cross[Id, inverse[S]]], INVERSE]]]

The statement obtained for the reflexive property is then transformed as follows:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], 
{u -> FUNS, 
        v -> fix[
            composite[INVERSE, inverse[image[inverse[COMPOSE], RFX]], 
              IMAGE[cross[Id, inverse[S]]]]], 
        w -> composite[COMPOSE, 
            intersection[composite[inverse[FIRST], INVERSE], 
              composite[inverse[SECOND], 
                IMAGE[cross[Id, inverse[S]]]]]]}]

% /. Equal -> SetDelayed

A similar restatement is obtained for the transitive property:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], 
{u -> FUNS, 
        v -> fix[
            composite[INVERSE, inverse[image[inverse[COMPOSE], TRV]], 
              IMAGE[cross[Id, inverse[S]]]]], 
        w -> composite[COMPOSE, 
            intersection[composite[inverse[FIRST], INVERSE], 
              composite[inverse[SECOND], 
                IMAGE[cross[Id, inverse[S]]]]]]}]

% /. Equal -> SetDelayed

the antitone property

Conversely, for any thin reflexive transitive relation x  there is a canonical factorization of the form  x = composite[inverse[funpart[y]], inverse[S], funpart[y]] where  y  is the restriction of the vertical section function to  fix[x].   For sets, this result is:

(equal[z,composite[inverse[funpart[y]],  inverse[S],  
                  funpart[y]]]/.y -> composite[VERTSECT[z], id[fix[z]]])/.z -> rfx[trv[setpart[x]]]

The variable  x  can be eliminated as follows.

SubstTest[class, x, 
        equal[image[u, singleton[setpart[x]]], 
          image[v, singleton[setpart[x]]]], 
{u -> 
            composite[COMPOSE, 
              intersection[composite[inverse[FIRST], INVERSE], 
                composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
              IMAGE[id[cart[V, V]]], VS, CORE[RFX], HULL[TRV], 
              IMAGE[id[cart[V, V]]]], 
          v -> composite[CORE[RFX], HULL[TRV], IMAGE[id[cart[V, V]]]]}] // 
      Reverse

% /. Equal -> SetDelayed

The wrapper-related functions  CORE[RFX]  and  composite[HULL[TRV], IMAGE[id[cart[V,V]]]] can be eliminated using  ImageComp:

Map[subclass[intersection[RFX, TRV], #] &, 
      ImageComp[composite[CORE[RFX], HULL[TRV], IMAGE[id[cart[V, V]]]], 
        inverse[composite[CORE[RFX], HULL[TRV], 
            IMAGE[id[cart[V, V]]]]], 
fix[
          composite[COMPOSE, 
            intersection[composite[inverse[FIRST], INVERSE], 
              composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
            VS]]]]

% /. Equal -> SetDelayed

The next step uses the fact that  VS  is contained in  cart[V, FUNS].  One needs this relation:

abstract[x, 
      fix[composite[COMPOSE, 
          intersection[composite[inverse[FIRST], INVERSE], 
            composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
          x]]]

The result is this inclusion:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], {u -> VS, 
        v -> cart[V, FUNS], 
        w -> composite[FIRST, 
            id[composite[
                intersection[composite[INVERSE, FIRST], 
                  composite[inverse[IMAGE[cross[Id, inverse[S]]]], SECOND]], 
                inverse[COMPOSE]]]]}]

% /. Equal -> SetDelayed

Combining this inclusion with the one derived for intersection[RFX, TRV] yields:

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, w], 
{u -> intersection[RFX, TRV], 
        v -> fix[
            composite[COMPOSE, 
              intersection[composite[inverse[FIRST], INVERSE], 
                composite[inverse[SECOND], IMAGE[cross[Id, inverse[S]]]]], 
              VS]], w -> 
          image[COMPOSE, 
            composite[IMAGE[cross[Id, inverse[S]]], id[FUNS], 
              INVERSE]]}]

% /. Equal -> SetDelayed

The reverse inclusion was proved in the preceding section. Combining these, one obtains a variable-free equation which says that (small) reflexive transitive relations can be characterized by the existence of a factorization of the form  composite[inverse[f], inverse[S], f] where  f  is a function.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> intersection[RFX, TRV], 
        v -> image[COMPOSE, 
            composite[IMAGE[cross[Id, inverse[S]]], id[FUNS], 
              INVERSE]]}]

image[COMPOSE, 
        composite[IMAGE[cross[Id, inverse[S]]], id[FUNS], INVERSE]] := 
      intersection[RFX, TRV]

Note the resemblance of this formula with a corresponding one for the class of equivalence relations:

image[COMPOSE, composite[id[FUNS], INVERSE]]