a strong form of reflexivity

Johan G. F. Belinfante
2008 February 12

SetDirectory["l:"]; <<  goedel.08feb10a; << tools.m

summary

This notebook is concerned with a careful study of the concept of a reflexive relation.  Patrick Suppes introduced the following definition for a strong form of reflexivity of a relation x on a set y.   (Actually, both x and y can be arbitrary classes here.)

assert[
      forall[t, implies[member[t, y], member[pair[t, t], x]]]]

Reference:  (see Definition 10 on page 69).

"Patrick Suppes, Axiomatic Set Theory, Dover Publications, New York, 1972.";

We shall say that x is strongly reflexive in y if the condition subclass[y, fix[x]] holds.  In the GOEDEL program, the (unary) predicate REFLEXIVE[x] is defined by the condition

subclass[x, cart[fix[x], fix[x]]]

In this notebook it is shown that if x is strongly reflexive in y, then the symmetric restriction intersection[x, cart[y,y]] is reflexive in the sense of the GOEDEL program, but not conversely.  The two conditions do agree for the special case that y is the union of the domain and range of x. This is usually called the field of x, but to avoid confusion with other meaning of the term field, the following acronym will be introduced for this union:

udora[x_] := union[domain[x], range[x]]

The restriction restrict[x, y, z] = intersection[x, cart[y, z]] of a relation is rewritten by the GOEDEL program as a composite:

intersection[x, cart[y, z]]

In particular, the symmetric restriction of a class x to the union of its domain and range is the relational part of x, that is, the class of all ordered pairs that belong to x.

restrict[x, udora[x], udora[x]]

strong reflexivity => reflexivity of the restriction

Lemma.

SubstTest[implies, equal[y, intersection[t, fix[x]]], 
        or[equal[0, 
            intersection[y, image[x, intersection[y, complement[fix[x]]]]]], 
          not[subclass[y, fix[x]]]], t -> y] // Reverse

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

Theorem.  Strong reflexivity implies reflexivity of the symmetric restriction.

or[not[subclass[y, fix[x]]], REFLEXIVE[composite[id[y], x, id[y]]]] // 
      AssertTest

or[not[subclass[y_, fix[x_]]], 
        REFLEXIVE[composite[id[y_], x_, id[y_]]]] := True

Counterexample.  The converse statement does not hold.  The strong assertion subclass[y, fix[x]] does not follow from the weaker statement REFLEXIVE[restrict[x,y,y]].

(implies[REFLEXIVE[composite[id[y], x, id[y]]], 
          subclass[y, fix[x]]]) /. {x -> EQUIDIFF, 
        y -> V}

Comment.  The statement that x is strongly reflexive on udora[x] is equivalent to the statement that the symmetric restriction of x to udora[x] is reflexive.

subclass[udora[x], fix[x]]

the class of sets for which the restriction of x is reflexive

In this section some properties of the class of sets on which the symmetric restriction of x is reflexive are derived.  The following formula for this class is readily derived:  fix[image[inverse[CART], image[inverse[IMAGE[id[x]]], RFX]]].  Indeed, one has:

member[y, 
      fix[image[inverse[CART], 
          image[inverse[IMAGE[id[x]]], RFX]]]]

Lemma.  Simplification rule.

subclass[intersection[y, image[inverse[x], w]], z] // AssertTest // 
      Reverse

equal[0, 
        intersection[w_, image[x_, intersection[y_, complement[z_]]]]] := 
      subclass[intersection[y, image[inverse[x], w]], z]

Theorem.  The statement that the restriction of x to y is symmetric can be rewritten as follows:

SubstTest[subclass, t, cartsq[fix[t]], t -> restrict[x, y, y]] // 
      Reverse

and[subclass[intersection[y_, image[x_, y_]], fix[x_]], 
        subclass[intersection[y_, image[inverse[x], y_]], fix[x_]]] := 
      REFLEXIVE[composite[id[y], x, id[y]]]

The class of sets y for which each of these inclusions holds is a class of cliques.  This explains the following normalization rule:

fix[image[inverse[CART], image[inverse[IMAGE[id[x]]], RFX]]] // 
        Normality // Reverse

intersection[cliques[union[cart[fix[x_], V], complement[x_]]], 
        cliques[union[cart[fix[x_], V], complement[inverse[x_]]]]] := 
      fix[image[inverse[CART], image[inverse[IMAGE[id[x]]], RFX]]]

Theorem.  Since classes of cliques are hereditary, the same holds for the class of sets for which the symmetric restriction of x is reflexive.

SubstTest[image, inverse[S], 
        intersection[cliques[u], 
          cliques[v]], 
{u -> 
            union[cart[fix[x], V], complement[x]], 
          v -> union[cart[fix[x], V], complement[inverse[x]]]}] // 
      Reverse

image[inverse[S], 
        fix[image[inverse[CART], image[inverse[IMAGE[id[x_]]], RFX]]]] := 
      fix[image[inverse[CART], image[inverse[IMAGE[id[x]]], RFX]]]

Lemma.

SubstTest[Uchains, cliques[t], t -> intersection[x, y]] // 
      Reverse

Uchains[intersection[cliques[x_], cliques[y_]]] := 
      intersection[cliques[x], cliques[y]]

Theorem.  Since classes of cliques are closed under chains of unions, the same holds for the class of sets for which the symmetric restriction of x is reflexive.

SubstTest[Uchains, 
        intersection[cliques[u], 
          cliques[v]], 
{u -> 
            union[cart[fix[x], V], complement[x]], 
          v -> union[cart[fix[x], V], complement[inverse[x]]]}] // 
      Reverse

Uchains[fix[image[inverse[CART], image[inverse[IMAGE[id[x_]]], RFX]]]] := 
      fix[image[inverse[CART], image[inverse[IMAGE[id[x]]], RFX]]]

Suppes’ problem 1, part (e) on page 78.

On page 78, problem 1, part (e), the reader is asked to show that a symmetric, transitive relation is reflexive.  This statement holds for the predicate REFLEXIVE as defined in the GOEDEL program.

implies[and[SYMMETRIC[x], TRANSITIVE[x]], REFLEXIVE[x]]

A version of this statement for restrictions of a relation x to a class y also holds, but a corresponding statement fails for the strong version of reflexivity, as shown by a counterexample.

Lemma.  (Temporary rewrite rule.)

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

equal[composite[id[y_], x_, id[y_]], 
        composite[id[y_], inverse[x_], id[y_]]] := 
      subclass[composite[id[y], inverse[x], id[y]], x]

Theorem.  If the restriction of a relation is symmetric and transitive, then it is reflexive.

Map[implies[#, REFLEXIVE[composite[id[y], x, id[y]]]] &, 
        SubstTest[and, SYMMETRIC[t], TRANSITIVE[t], 
          t -> restrict[x, y, y]]] // Reverse

or[not[subclass[composite[id[y_], inverse[x_], id[y_]], x_]], 
        not[TRANSITIVE[composite[id[y_], x_, id[y_]]]], 
        REFLEXIVE[composite[id[y_], x_, id[y_]]]] := True

Counterexample.   If the restriction of a relation is symmetric and transitive, it need not be reflexive in the stronger sense.

(or[not[subclass[composite[id[y], inverse[x], id[y]], x]], 
          not[TRANSITIVE[composite[id[y], x, id[y]]]], 
          subclass[y, fix[x]]]) /. {x -> EQUIDIFF, 
        y -> V}

Corollary.  For the case of y = udora[x], one finds:

SubstTest[or, not[subclass[composite[id[y], inverse[x], id[y]], x]], 
        not[TRANSITIVE[composite[id[y], x, id[y]]]], 
        REFLEXIVE[composite[id[y], x, id[y]]], y -> udora[x]] // 
      Reverse

or[not[subclass[inverse[x_], x_]], not[TRANSITIVE[composite[Id, x_]]], 
        REFLEXIVE[composite[Id, x_]]] := True