associative relations

Johan G. F. Belinfante
2003 July 2

<< goedel52.s31; << tools.m

summary

A formula for the class of all associative relations is verified.

preliminaries

To speed up the computation, some flags are turned off.

cond = False; simplify = False;

The class of associative relations is defined by this membership rule:

member[x, ASSOCIATIVE]

lemmas

To clean up some formulas, it helps to add this rule:

equal[composite[x, cross[x, Id]], composite[x, cross[Id, x], ASSOC]]
           // AssertTest // Reverse

and[
        subclass[composite[x_, cross[Id, x_], ASSOC], 
          composite[x_, cross[x_, Id]]], 
        subclass[composite[x_, cross[x_, Id], inverse[ASSOC]], 
          composite[x_, cross[Id, x_]]], 
        subclass[image[inverse[x_], domain[domain[x_]]], cart[V, V]]] := 
      equal[composite[x, cross[x, Id]], composite[x, cross[Id, x], ASSOC]]

A formula discovered earlier this morning can almost be verified at this point:

\(member[x, 
        intersection[P[cart[cart[V, V], V]], 

          fix[image[inverse[CART], 
              fix[composite[
                  inverse[
                    IMAGE[composite[SWAP, RIF, 
                        cross[Id, 
                          composite[cross[SWAP, Id], inverse[RIF]]]]]], 
                  IMAGE[composite[SWAP, RIF, 
                      cross[Id, 
                        composite[cross[inverse[ASSOC], SWAP], 
                          inverse[RIF]]]]]]]]]]] // assert\)

The following theorem cleans this up further:

\(Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], not[implies[p1, p3]], 
        
		{p1 -> member[x, V], p2 -> member[domain[x], V], 
          p3 -> member[image[domain[x], y], V]}]]\)

or[member[image[domain[x_], y_], V], not[member[x_, V]]] := True

Thus:

equiv[and[member[x, V], member[image[domain[x], y], V]], member[x, V]]

The simpliest procedure is to make this a temporary rewrite rule:

and[member[x_, V], member[image[domain[x_], y_], V]] := member[x, V]

verification

(ASSOCIATIVE // Normality // Reverse) /. Equal -> SetDelayed

intersection[P[cart[cart[V, V], V]], 
        fix[image[inverse[CART], 
            fix[composite[
                inverse[
                  IMAGE[composite[SWAP, RIF, 
                      cross[Id, composite[cross[SWAP, Id], inverse[RIF]]]]]], 
                IMAGE[composite[SWAP, RIF, 
                    cross[Id, 
                      composite[cross[inverse[ASSOC], SWAP], 
                        inverse[RIF]]]]]]]]]] // Renormality

intersection[
        fix[image[inverse[CART], 
            fix[composite[
                inverse[
                  IMAGE[composite[SWAP, RIF, 
                      cross[Id, composite[cross[SWAP, Id], inverse[RIF]]]]]], 
                IMAGE[composite[SWAP, RIF, 
                    cross[Id, 
                      composite[cross[inverse[ASSOC], SWAP], 
                        inverse[RIF]]]]]]]]], P[cart[cart[V, V], V]]] := 
      ASSOCIATIVE

some clues about how the formula was discovered

The following results were discovered using reification.  These formulas formed the basis of the discovery of the formula verified above.  The two functions inside IMAGE in the formula above convert cart[x,x]  to the left and right sides of the associativity condition.

image[
      composite[SWAP, RIF, 
        cross[Id, composite[cross[SWAP, Id], inverse[RIF]]]], cart[x, x]]

image[
      composite[SWAP, RIF, 
        cross[Id, composite[cross[inverse[ASSOC], SWAP], inverse[RIF]]]], 
      cart[x, x]]

This observation allows one to consider the associative law as a condition satisfied by cart[x,x], thereby effectively replacing four occurrences of the variable  x  in the associative law by two occurrences of the cartesian square  cart[x,x].  The formula says that  x  is associative if its cartesian square is a fixed point of some relation.

thin-ness  results

The two relations involved in the formula for  ASSOCIATIVE  are thin:

domain[
        VERTSECT[
          composite[SWAP, RIF, 
            cross[Id, composite[cross[SWAP, Id], inverse[RIF]]]]]] // 
      Normality

domain[
        VERTSECT[
          composite[SWAP, RIF, 
            cross[Id, composite[cross[inverse[ASSOC], SWAP], inverse[RIF]]]]]]
         // Normality