thin transitive relations

Johan G. F. Belinfante
2004 June 5

SetDirectory["c:/goedel/goedel/2004/jun/05"]; << goedel58.05a; << 
      tools.m

summary

It is shown in this notebook that  thinpart[trv[x]] and  trv[thinpart[x]] are generic thin transitive relations.  That is, the composition of the thinpart and trv wrappers in either order act as wrappers for thin transitive relations.  A counterexample is presented that shows that thinpart and trv in general do not commute.

thinness results

An equality substition rule holds for thin:

implies[and[equal[x, y], thin[y]], thin[x]] // AssertTest

or[equal[V, domain[VERTSECT[x_]]], not[equal[V, domain[VERTSECT[y_]]]], 
        not[equal[x_, y_]]] := True

Corollary:

SubstTest[implies, and[equal[x, z], thin[z]], thin[x], 
      z -> thinpart[y]]

or[equal[V, domain[VERTSECT[x_]]], not[equal[x_, thinpart[y_]]]] := 
      True

The transitive closure of a relation is thin if and only if the relation itself is thin.

SubstTest[implies, and[subclass[u, v], thin[v]], 
      thin[u], {u -> composite[Id, x], v -> trv[x]}]

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

equiv[equal[V, domain[VERTSECT[x]]], 
      equal[V, domain[VERTSECT[trv[x]]]]]

Restatement:

equiv[thin[trv[x]], thin[x]]

This will be added as a new rewrite rule:

equal[V, domain[VERTSECT[trv[x_]]]] := 
      equal[V, domain[VERTSECT[x]]]

It is natural to ask at this point whether domain[VERTSECT[trv[x]]] and domain[VERTSECT[x]] are equal.  In the last section of this notebook, a counterexample is presented that shows this is not generally true.

an antitone property

In this section it is shown that if two elements are related by a transitive relation, then their vertical sections are related by the inverse subset relation.  The following lemma yields a rewrite rule whose orientation  is opposite to another one in which the inverse and complement are omitted, but that should nonethless not deter one from adding this rule because that rule also has subclass replaced with a disjointness assertion, thereby preventing pattern matching with the present rule.

member[pair[u, v], composite[inverse[x], complement[x]]] // 
      AssertTest

member[pair[u_, v_], composite[inverse[x_], complement[x_]]] := 
      and[member[u, V], 
        not[subclass[image[x, singleton[v]], 
            image[x, singleton[u]]]]]

Theorem: the antitone property for vertical sections of a transitive relation:

\(Map[or[#, subclass[image[x, singleton[v]], image[x, singleton[u]]]] &, 
      SubstTest[implies, and[member[y, x], subclass[x, z]], 
        member[y, z], 
	{y -> pair[u, v], 
          z -> composite[Id, 
              complement[composite[inverse[x], complement[x]]]]}]]\)

or[not[member[pair[u_, v_], x_]], not[TRANSITIVE[x_]], 
        subclass[image[x_, singleton[v_]], image[x_, singleton[u_]]]] := 
      True

The following corollary eliminates the TRANSITIVE predicate by replacing it with a trv wrapper.

\(SubstTest[implies, and[TRANSITIVE[y], member[pair[u, v], y]], 
	
      subclass[image[y, singleton[v]], image[y, singleton[u]]], 
      y -> trv[x]]\)

or[not[member[pair[u_, v_], trv[x_]]], 
        subclass[image[trv[x_], singleton[v_]], 
          image[trv[x_], singleton[u_]]]] := True

thin part of a transitive relation

Applying the subset theorem yields:

\(Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p2, p3], p4], 
        not[implies[and[p1, p3], p4]], {p1 -> member[pair[u, v], trv[x]], 
          p2 -> subclass[image[trv[x], singleton[v]], 
              image[trv[x], singleton[u]]], 
	
          p3 -> member[image[trv[x], singleton[u]], V], 
          p4 -> member[image[trv[x], singleton[v]], V]}]]\)

(% /. {x -> x_, u -> u_, v -> v_}) /. 
      Equal -> SetDelayed

Removing the variables  u  and  v  yields this reformulation:

Map[equal[0, composite[Id, complement[#]]] &, 
        SubstTest[class, pair[u, v], 
          or[member[image[t, singleton[v]], V], 
            not[member[image[t, singleton[u]], V]], 
            not[member[pair[u, v], t]]], t -> trv[x]]] // Reverse

subclass[U[range[VERTSECT[trv[x_]]]], domain[VERTSECT[trv[x_]]]] := 
      True

From this one can deduce that the thin part of a transitive relation is transitive:

SubstTest[implies, and[TRANSITIVE[z], invariant[z, w]], 
      TRANSITIVE[composite[z, id[w]]], {z -> trv[x], 
        w -> domain[VERTSECT[trv[x]]]}]

TRANSITIVE[thinpart[trv[x_]]] := True

Corollary 1.

equal[trv[thinpart[trv[x]]], thinpart[trv[x]]]

trv[thinpart[trv[x_]]] := thinpart[trv[x]]

Corollary 2:

SubstTest[implies, and[equal[x, y], TRANSITIVE[y]], TRANSITIVE[x], 
      y -> thinpart[trv[x]]]

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

the wrapper results

Lemma:

SubstTest[implies, and[equal[x, y], equal[y, z]], 
      equal[x, z], {y -> trv[x], z -> thinpart[trv[x]]}]

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

First main result: thinpart[trv[x]] is a generic thin transitive relation.

equiv[equal[x, thinpart[trv[x]]], and[thin[x], TRANSITIVE[x]]] // 
        not // not

equal[x_, thinpart[trv[x_]]] := 
      and[equal[V, domain[VERTSECT[x]]], TRANSITIVE[x]]

The next goal is to show that one can interchangie the order of thinpart and trv.  Some lemmas are needed:

SubstTest[implies, equal[x, thinpart[y]], thin[x], 
      y -> trv[thinpart[x]]]

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

SubstTest[implies, and[equal[x, y], TRANSITIVE[y]], TRANSITIVE[x], 
      y -> trv[thinpart[x]]]

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

SubstTest[implies, and[equal[x, y], equal[y, z]], 
      equal[x, z], 
{y -> trv[x], 
        z -> trv[thinpart[x]]}]

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

SubstTest[implies, equal[x, y], equal[trv[x], trv[y]], 
      y -> thinpart[x]]

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

Map[not, 
      SubstTest[and, implies[p2, p3], implies[and[p1, p3], p4], 
        not[implies[and[p1, p2], p4]], {p1 -> equal[x, trv[x]], 
          p2 -> equal[x, thinpart[x]], 
          p3 -> equal[trv[x], trv[thinpart[x]]], 
          p4 -> equal[x, trv[thinpart[x]]]}]]

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

Second main result:  trv[thinpart[x]] is a also a generic thin transitive relation.

equiv[equal[x, trv[thinpart[x]]], and[thin[x], TRANSITIVE[x]]] // 
        not // not

equal[x_, trv[thinpart[x_]]] := 
      and[equal[V, domain[VERTSECT[x]]], TRANSITIVE[x]]

a counterexample

A natural question is whether  trv[thinpart[x]]  and  thinpart[trv[x]]  are always equal.   The following counterexample shows that in general, the functors trv and thinpart do not commute.

example = 
        union[cart[singleton[0], singleton[singleton[0]]], 
          cart[complement[singleton[0]], V]];

thinpart[example] // Normality

% /. Equal -> SetDelayed

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

% /. Equal -> SetDelayed

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> trv[example], 
        v -> cart[V, V]}]

trv[
        union[cart[complement[singleton[0]], V], 
          cart[singleton[0], singleton[singleton[0]]]]] := 
      cart[V, V]

This example also shows that in general domain[VERTSECT[x]] and domain[VERTSECT[trv[x]]] need not be equal, answering a question raised earlier.

domain[VERTSECT[trv[example]]]

domain[VERTSECT[example]]

equal[domain[VERTSECT[trv[example]]], 
      domain[VERTSECT[example]]]

Lemma.

setpart[V] // Normality

setpart[V] := 0

The thinpart ot trv[example] is empty:

thinpart[trv[example]]

The example shows that  trv and thinpart do not commute:

equal[trv[thinpart[example]], thinpart[trv[example]]]