asymmetric part of a transitive relation

Johan G. F. Belinfante
2009 May 19

SetDirectory["l:"]; << goedel.09may18a; << tools.m

summary

The asymmetric part of a transitive relation is transitive:

implies[TRANSITIVE[x], TRANSITIVE[dif[x, inverse[x]]]]

In this notebook a variable-free expression of this fact is derived for the special case of transitive relations that are sets.  A particularly nice formulation of this uses the idempotent function composite[DIF, id[INVERSE], inverse[FIRST]].

derivation

The best results are obtained if the function IMAGE[SWAP] which takes x to inverse[x] is replaced with its restriction INVERSE.

Lemma.  The class of transitive relations is contained in the class of relations whose asymmetric part is transitive.

Map[subclass[TRV, intersection[P[cart[V, V]], #]] &, 
        union[complement[TRV], 
            fix[composite[inverse[image[inverse[DIF], TRV]], IMAGE[SWAP]]]] // 
          Normality] // InvertFix

% /. Equal -> SetDelayed

Lemma.  The asymmetric part of a transitive relation is transitive.

SubstTest[subclass, intersection[y, domain[funpart[x]]], 
      image[inverse[funpart[x]], 
        z], {x -> composite[DIF, id[INVERSE], inverse[FIRST]], 
        y -> TRV, z -> TRV}]

% /. Equal -> SetDelayed

Lemma.  Simplification rule.

fix[composite[complement[inverse[E]], INVERSE, id[TRV], E]] // 
      Normality

fix[composite[complement[inverse[E]], INVERSE, id[TRV], E]] := 
      Di

Lemma.  An irreflexive transitive relation is its own asymmetric part.

SubstTest[implies, subclass[y, fix[funpart[x]]], 
        equal[image[funpart[x], y], 
          y], {x -> composite[DIF, id[INVERSE], inverse[FIRST]], 
          y -> intersection[TRV, P[Di]]}] // Reverse

image[DIF, composite[INVERSE, id[intersection[TRV, P[Di]]]]] := 
      intersection[TRV, P[Di]]

Lemma.  Every irreflexive transitive relation is the asymmetric part of a transitive relation.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], 
          image[t, v]], {t -> 
            composite[DIF, id[INVERSE], inverse[FIRST]], 
          u -> intersection[TRV, P[Di]], v -> TRV}] // 
      Reverse

% /. Equal -> SetDelayed

Theorem.   The class of asymmetric parts of transitive relations is equal to the class of irreflexive transitive relations.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> intersection[TRV, P[Di]], 
        v -> image[DIF, composite[INVERSE, id[TRV]]]}]

image[DIF, composite[INVERSE, id[TRV]]] := 
      intersection[TRV, P[Di]]