the PS machine versus VERTSECT

Johan G. F. Belinfante
2004 April 22

<< goedel56.20a;  <<  tools.m;

summary

The use of  PS  and  VERTSECT  both provide methods of cancelling factors of  S  and inverse[S] from formulas for functions. The formulas used in the Otter work to define BIGCAP and POWER made use of the proper subset relation PS.  This notebook compares these constructions with alternate formulas using VERTSECT that would perhaps have led to simpler definitions.

three new rewrite rules

To simplify the discussion it is useful to add a few new rewrite rules.  The following is just the inverse of an existing rule:

intersection[complement[composite[inverse[PS], inverse[S]]], 
        inverse[S]] // DoubleInverse

intersection[complement[composite[inverse[PS], inverse[S]]], 
        inverse[S]] := Id

The following identities involve VERTSECT.

complement[composite[complement[E], x]] // VSNormality

It is all right to omit the factor of  Id  here.

composite[complement[composite[complement[E], x_]]] := 
      composite[S, VERTSECT[x]]

One could add a rule of this sort, but one can do better:

complement[composite[complement[E], x]] // Normality

complement[composite[complement[E], x_]] := 
      union[complement[cart[V, V]], composite[S, VERTSECT[x]]]

intersection[composite[S, VERTSECT[x]], composite[complement[E], x]] // 
      VSNormality

intersection[composite[S, VERTSECT[x_]], composite[complement[E], x_]] := 
      0

the Otter definitions of BIGCAP and POWER

The definition of BIGCAP in the Otter work amounts to this formula:

dif[LB[S], composite[inverse[PS], LB[S]]]

The relation inverse[LB[S]] was called LOWERBOUND in the Otter work.  The function BIGCAP could also have been recovered from LB[S] as follows:

composite[BIGCUP, VERTSECT[LB[S]]]

Both of these constructions are examples of general methods for cancelling a factor of inverse[S]:

composite[BIGCUP, VERTSECT[#]] & @ 
      composite[inverse[S], ff]

dif[#, composite[inverse[PS], #]] & @ 
      composite[inverse[S], ff]

A simpler formula for BIGCAP is this:

VERTSECT[LB[E]]

A similar technique could have been used to define POWER, but the Otter work but did not use this:

dif[#, composite[inverse[PS], #]] & @ inverse[UB[S]]

Instead the following relation was used in the Otter work.

SUPERPOWER  == 
      composite[Id, 
        complement[composite[complement[E], inverse[S]]]]

The following proper-subset relation was used to cancel the factor of  S, using the following general observation:

intersection[#, complement[composite[PS, #]]] & @ 
      composite[S, ff]

Thus, in light of the rewrite rule derived in the preceding section, the Otter formula amounts to this:

intersection[#, complement[composite[PS, #]]] & @ 
      composite[S, VERTSECT[inverse[S]]]

A simpler method would have been to use the following formula that appears in work by Formisano and Omeodeo:

VERTSECT[inverse[S]]

The reference is this:

"Andrea Formisano, Eugenio G.Omodeo: An Equational Re-engineering of \
Set Theories.
 in Automated Deduction in Classical and Non-Classical Logics: Selected \
Papers
Editors: R. Caferra, G. Salzer (Eds.):  FTP (LNCS vol 1761/2000) 1998: \
pp.175-190"

The function  BIGCUP could have been constructed in a similar way, using a double application of complement.

VERTSECT[complement[LB[complement[E]]]]

Note however that

VERTSECT[complement[LB[complement[x]]]]

So this amounts to using the formula that was used in the Otter work:

IMAGE[inverse[E]]