APPLY and rotate[E]

Johan G. F. Belinfante
2003 May 12

<< goedel52.r67; << tools.m

introduction

The class APPLY[x,y] is a shorthand for

APPLY[x, y]

This constructor is mainly useful for applying a function to an argument.  Applying  lambda  to this expression yields a formula involving the rotated membership relation  rotate[E].  This formula involves the function  BIGCAP  which corresponds to the constructor  A[x]:

class[y, forall[z, implies[member[z, x], member[y, z]]]]

lambda[x, A[x]]

For function evaluation, the purpose of  BIGCAP  is to extract the value of a function from the singleton produced by taking the vertical section  image[x,singleton[y]] of a function  x  at an argument  y.  The unary intersection operation   A  is not the only way to extract an element from its singleton.  It is often desirable, when dealing with functions, to replace the function   BIGCAP  with  inverse[SINGLETON].  In this notebook some formulas are derived which show how to go about doing this.  These formula involve the function  FUNPART:

lambda[x, funpart[x]]

The constructor  funpart  is defined by

intersection[composite[Id, x], complement[composite[Di, x]]]

This constructor is useful for eliminating  FUNCTION  hypotheses from clauses.

equal[x, funpart[x]]

One can therefore think of the expression  funpart[x]  as a generic function.

applying lambda to APPLY

Applying lambda to the constructor  APPLY  yields the binary function

lambda[pair[x, y], APPLY[x, y]]

The rotated membership relation in this formula can be eliminated:

composite[complement[inverse[E]], BIGCAP, IMG, cross[Id, SINGLETON]] // 
        VSTriNormality // Reverse

composite[complement[inverse[E]], 
        rotate[E]] := 
      composite[complement[inverse[E]], BIGCAP, IMG, 
        cross[Id, SINGLETON]]

The formula for lambda APPLY now produces a more transparent result:

lambda[pair[x, y], APPLY[x, y]]

special formulas for function evaluation

For the application to function evaluation, one can replace BIGCAP by  inverse[SINGLETON].  In this section, some formulas are derived which show how to do this.

Map[VERTSECT[complement[#]] &, 
      composite[complement[inverse[E]], BIGCAP, IMG, 
          cross[FUNPART, SINGLETON]] // TriNormality]

The add-on appearing on the right side is the empty set in disguise:

SubstTest[composite, id[range[x]], x, 
        x -> cart[
            intersection[
              composite[inverse[SINGLETON], 
                complement[image[inverse[IMG], range[SINGLETON]]]], 
              composite[inverse[E], IMAGE[FIRST], FUNPART]], 
            singleton[0]]] // Reverse

cart[
        intersection[
          composite[inverse[SINGLETON], 
            complement[image[inverse[IMG], range[SINGLETON]]]], 
          composite[inverse[E], IMAGE[FIRST], FUNPART]], 
        singleton[0]] := 0

The formula derived above now simplifies to

%12

composite[BIGCAP, IMG, cross[FUNPART, SINGLETON]] := 
      composite[inverse[SINGLETON], IMG, cross[Id, SINGLETON]]

Another interesting formula for this function  is obtained by a triple rotation:

composite[rotate[E], cross[FUNPART, Id]] // 
      TripleRotate

composite[rotate[E], cross[FUNPART, Id]] := 
      composite[inverse[SINGLETON], IMG, cross[Id, SINGLETON]]