a substitute for Quaife's Theorem AP-11

Johan G. F. Belinfante and Tiffany Goble
2004 January 22

<<  goedel53.22b; << tools.m

summary

A substitute is derived for Quaife's theorem AP-11 with APPLY in place of apply.  Recall the definitions:

apply[x, y]  ==  U[image[x, singleton[y]]]

APPLY[x, y] == A[image[x, singleton[y]]]

The literal about the domain in Quaife's theorem is not needed for the substitute theorem.

derivation

Lemma 1.

SubstTest[implies, equal[w, y], 
      equal[composite[x, w], composite[x, y]], 
      w -> funpart[y]]

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

Lemma 2.

SubstTest[implies, equal[u, v], 
      equal[APPLY[u, z], APPLY[v, z]], {u -> composite[x, y], 
        v -> composite[x, funpart[y]]}]

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

Lemma 3.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], {p1 -> FUNCTION[y], 
          p2 -> equal[composite[x, y], composite[x, funpart[y]]], 
          p3 -> 
            equal[APPLY[composite[x, y], z], 
              APPLY[x, APPLY[funpart[y], z]]]}]]

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

The substitute theorem:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p3, p4], 
        implies[and[p2, p4], p5], 
        not[implies[p1, p5]], {p1 -> FUNCTION[y], 
          p2 -> equal[APPLY[composite[x, funpart[y]], z], 
              APPLY[composite[x, y], z]], 
          p3 -> equal[APPLY[funpart[y], z], APPLY[y, z]], 
          p4 -> 
            equal[APPLY[x, APPLY[funpart[y], z]], APPLY[x, APPLY[y, z]]], 
          p5 -> equal[APPLY[composite[x, y], z], 
              APPLY[x, APPLY[y, z]]]}]]

or[equal[A[image[x_, image[y_, singleton[z_]]]], 
          APPLY[x_, APPLY[y_, z_]]], not[FUNCTION[y_]]] := True

Restatement:

or[not[FUNCTION[y]], 
      equal[APPLY[composite[x, y], z], APPLY[x, APPLY[y, z]]]]