some rewrite rules for transitive relations

Johan G. F. Belinfante
2004 March 21

<< goedel55.20a;  <<  tools.m;

summary

This notebook contains replacements for some rewrite rules that had to be removed after wrapping the definition of TRANSITIVE  with class.  Some new results about transitive relations were discovered in the process.

transitive closure

In this section it is shown that  x  is transitive if and only if it is its own transitive closure.  Rather than following the rather roundabout derivation that had been used in a notebook dated 2002 March 21, an easier way to do this will be presented.  The basis for the new approach is to use facts about iteration, beginning with the following fact:

\(SubstTest[implies, 
      and[equal[image[w, singleton[0]], v], 
        equal[composite[u, w], composite[w, SUCC]]], 
      equal[iterate[u, v], composite[w, id[omega]]], 
	{u -> cross[Id, x], 
        v -> composite[Id, y], 
        w -> composite[cross[inverse[y], Id], power[x]]}]\)

This is made into a temporary rewrite rule:

iterate[cross[Id, x_], composite[Id, y_]] := 
      composite[cross[inverse[y], Id], power[x]]

Taking the image with complement[singleton[0]] yields an equation involving transitive closures:

SubstTest[image, iterate[z, w], 
        complement[singleton[0]], {w -> composite[Id, y], 
          z -> cross[Id, x]}] // Reverse

image[trv[cross[Id, x_]], composite[Id, y_]] := 
      composite[trv[x], y]

Theorem.

SubstTest[subclass, range[iterate[u, v]], 
      v, {u -> cross[Id, x], v -> composite[Id, y]}]

subclass[composite[trv[x_], y_], y_] := 
      subclass[composite[x, y], y]

Specializing to the case that  y  is  x  yields:

SubstTest[subclass, composite[trv[x], y], y, y -> x]

subclass[composite[trv[x_], trv[x_]], x_] := 
      TRANSITIVE[composite[Id, x]]

Theorem.

SubstTest[subclass, union[u, v], 
      x, {u -> composite[Id, x], v -> composite[trv[x], trv[x]]}]

subclass[trv[x_], x_] := TRANSITIVE[composite[Id, x]]

It follows that a relation is transitive if it is its own transitive closure.

equal[x, trv[x]] // AssertTest

equal[x_, trv[x_]] := TRANSITIVE[x]

This result can be used to derive some substitution theorems:

SubstTest[implies, and[equal[w, x], subclass[x, y]], subclass[w, y], 
      w -> trv[x]]

or[not[subclass[x_, y_]], not[TRANSITIVE[x_]], subclass[trv[x_], y_]] := 
      True

\(SubstTest[implies, and[subclass[u, v], equal[v, w]], 
      subclass[u, w], 
	{u -> x, v -> y, w -> trv[y]}]\)

or[not[subclass[x_, y_]], not[TRANSITIVE[y_]], subclass[x_, trv[y_]]] := 
      True

Lemma.

\(SubstTest[implies, and[subclass[u, v], equal[v, w]], 
      subclass[u, w], 
	{u -> trv[x], v -> trv[y], w -> y}]\)

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

Theorem:  If  x  is contained in a transitive relation, then so is its transitive closure.

\(Map[not, 
      SubstTest[and, implies[p1, p3], implies[and[p2, p3], p4], 
        not[implies[and[p1, p2], p4]], 
		{p1 -> subclass[x, y], 
          p2 -> TRANSITIVE[y], p3 -> subclass[trv[x], trv[y]], 
          p4 -> subclass[trv[x], y]}]]\)

or[not[subclass[x_, y_]], not[TRANSITIVE[y_]], subclass[trv[x_], y_]] := 
      True

Corollary:  The transitive closure of E is the smallest transitive relation that contains E.

SubstTest[implies, and[subclass[w, x], TRANSITIVE[x]], 
      subclass[trv[w], x], w -> E]

or[not[subclass[E, x_]], not[TRANSITIVE[x_]], 
        subclass[composite[inverse[TC], E], x_]] := True

Another related result:

equal[composite[Id, x], trv[x]] // AssertTest

equal[composite[Id, x_], trv[x_]] := 
      TRANSITIVE[composite[Id, x]]

serendipity

The following additional result about iterate was discovered in the course of deriving the results in the previous section.

\(SubstTest[implies, 
      and[equal[image[w, singleton[0]], v], 
        equal[composite[u, w], composite[w, SUCC]]], 
      equal[iterate[u, v], composite[w, id[omega]]], 
	{u -> x, v -> y, 
        w -> cart[omega, y]}]\)

or[equal[cart[omega, y_], iterate[x_, y_]], 
        not[equal[y_, image[x_, y_]]]] := True

irreflexive part of a transitive relation

The following fact was recently used to show that well-orderings are transitive.

subclass[composite[intersection[Di, x], intersection[Di, x]], x] // 
      AssertTest

subclass[composite[intersection[Di, x_], intersection[Di, x_]], x_] := 
      TRANSITIVE[composite[Id, x]]

intersection of transitive relations

The following basic result has been derived previously:

implies[and[TRANSITIVE[x], TRANSITIVE[y]], 
      TRANSITIVE[intersection[x, y]]]

The goal of this section is to weaken the hypothesis slightly.  It suffices to assume that only one of the two classes  x  and  y  is a relation.  Some lemmas are needed:

\(SubstTest[implies, subclass[u, x], 
      subclass[composite[u, u], composite[x, x]], 
	
      u -> intersection[x, y]]\)

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

Lemma.

\(SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, 
        w], 
	{u -> composite[intersection[x, y], intersection[x, y]], 
        v -> composite[x, x], w -> x}]\)

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

Lemma.

Map[not, 
        SubstTest[subclass, composite[w, w], intersection[x, y], 
          w -> intersection[x, y]]] // Reverse

or[not[
          subclass[composite[intersection[x_, y_], intersection[x_, y_]], 
            x_]], not[
          subclass[composite[intersection[x_, y_], intersection[x_, y_]], 
            y_]]] := not[
        TRANSITIVE[composite[Id, intersection[x, y]]]]

Theorem.

\(Map[not, 
      SubstTest[and, implies[p1, p3], implies[p1, p4], implies[p2, p6], 
        implies[p4, p5], implies[p3, p7], implies[and[p5, p6, p7], p8], 
        not[implies[and[p1, p2], p8]], {p1 -> TRANSITIVE[x], 
          p2 -> TRANSITIVE[composite[Id, y]], p3 -> subclass[x, cart[V, V]], 
          p4 -> TRANSITIVE[composite[Id, x]], 
			p5 -> 
            subclass[composite[intersection[x, y], intersection[x, y]], x], 
          p6 -> subclass[composite[intersection[x, y], intersection[x, y]], 
              y], p7 -> subclass[intersection[x, y], cart[V, V]], 
			p8 -> 
            TRANSITIVE[intersection[x, y]]}]]\)

or[not[TRANSITIVE[x_]], not[TRANSITIVE[composite[Id, y_]]], 
        TRANSITIVE[intersection[x_, y_]]] := True

an equality substitution theorem

The following theorem is mainly of interest in the special case that  z  is  Id, but the general case is no more difficult to establish.

\(Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p2, p3], p4], 
          not[implies[and[p1, p3], p4]], 
		{p1 -> equal[x, y], 
            p2 -> equal[composite[z, x], composite[z, y]], 
            p3 -> TRANSITIVE[composite[z, x]], 
            p4 -> TRANSITIVE[composite[z, y]]}]] // MapNotNot\)

or[not[equal[x_, y_]], not[TRANSITIVE[composite[z_, x_]]], 
        TRANSITIVE[composite[z_, y_]]] := True

an intersection theorem involving TRV.

Lemma.

implies[and[TRANSITIVE[composite[Id, x]], member[y, TRV]], 
        member[intersection[x, y], TRV]] // NotNotTest

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

The following general theorem holds:

Map[equal[V, #] &, 
        SubstTest[class, y, 
          implies[and[TRANSITIVE[composite[Id, x]], member[y, z]], 
            member[intersection[x, y], z]], z -> TRV]] // Reverse

or[not[TRANSITIVE[composite[Id, x_]]], 
        subclass[image[IMAGE[id[x_]], TRV], TRV]] := True

The following corollary is more memorable:

\(Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], 
		{p1 -> TRANSITIVE[x], 
          p2 -> TRANSITIVE[composite[Id, x]], 
          p3 -> subclass[image[IMAGE[id[x]], TRV], TRV]}]]\)

or[not[TRANSITIVE[x_]], subclass[image[IMAGE[id[x_]], TRV], TRV]] := 
      True

intersection of transitive closures

SubstTest[implies, and[TRANSITIVE[u], TRANSITIVE[v]], 
      TRANSITIVE[intersection[u, v]], {u -> trv[x], v -> trv[y]}]

TRANSITIVE[intersection[trv[x_], trv[y_]]] := True

assessment

Lemma.

SubstTest[implies, and[FUNCTION[z], member[x, domain[z]]], 
      member[APPLY[z, x], range[z]], z -> HULL[TRV]]

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

The converse also holds:

\(SubstTest[implies, and[TRANSITIVE[u], equal[u, v]], 
      TRANSITIVE[v], 
	{u -> A[intersection[TRV, image[S, singleton[x]]]], 
        v -> V}]\)

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

These facts can be combined:

equiv[and[member[x, V], subclass[x, cart[V, V]]], 
      TRANSITIVE[A[intersection[TRV, image[S, singleton[x]]]]]]

TRANSITIVE[A[intersection[TRV, image[S, singleton[x_]]]]] := 
      and[member[x, V], subclass[x, cart[V, V]]]

A related result will be derived.

SubstTest[implies, TRANSITIVE[w], TRANSITIVE[composite[Id, w]], 
      w -> A[intersection[TRV, image[S, singleton[x]]]]]

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

\(SubstTest[implies, and[TRANSITIVE[composite[Id, u]], equal[u, v]], 
      TRANSITIVE[composite[Id, v]], 
	{u -> V, 
        v -> A[intersection[TRV, image[S, singleton[x]]]]}]\)

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

The above results can be combined:

\(SubstTest[and, implies[p, q], 
        implies[not[p], 
          q], 
	{p -> and[member[x, V], subclass[x, cart[V, V]]], 
          q -> TRANSITIVE[
              composite[Id, A[intersection[TRV, image[S, singleton[x]]]]]]}] // 
      Reverse\)

TRANSITIVE[
        composite[Id, A[intersection[TRV, image[S, singleton[x_]]]]]] := 
      True

a connection between TRV and binclosed[COMPOSE]

image[inverse[POWER], binclosed[COMPOSE]] // Normality

A similar result holds without the assumption that  x  be a set.

subclass[U[image[COMPOSE, cart[P[x], P[x]]]], x]