some theorems about range and image

Johan G. F. Belinfante and Tiffany D. Goble
2004 February 28

<< goedel54.28a;  <<  tools.m

summary

In this notebook some results related to Quaife's classics on range and image are derived.   All of these are simple theorems that were proven several years ago using McCune's automated theorem proving program Otter, but which until now were not immediately recognized to be true by the GOEDEL program.

a corollary of Quaife's theorem (RA8)

Quaife's first corollary of his Theorem  (RA8)  is transformed as follows by the GOEDEL program:

subclass[range[restrict[x, y, z]], 
      intersection[range[x], z]]

This result can be established as follows:

subclass[intersection[z, image[x, y]], range[x]] // 
      AssertTest

subclass[intersection[z_, image[x_, y_]], range[x_]] := True

a result related to Quaife's theorem (IM2)

Lemmas.

Map[or[member[u, x], #] &, 
      SubstTest[implies, and[member[z, w], subclass[w, t]], 
        member[z, t], {z -> pair[u, v], t -> cart[x, y]}]]

or[member[u_, x_], not[member[pair[u_, v_], w_]], 
        not[subclass[w_, cart[x_, y_]]]] := True

Map[or[member[v, y], #] &, 
      SubstTest[implies, and[member[z, w], subclass[w, t]], 
        member[z, t], {z -> pair[u, v], t -> cart[x, y]}]]

or[member[v_, y_], not[member[pair[u_, v_], w_]], 
        not[subclass[w_, cart[x_, y_]]]] := True

The following result generalizes Theorem IM-2B, a corollary of Quaife's theorem (IM2) that was proved 1998 May 3 using Otter.

Map[not, 
      SubstTest[and, implies[and[p2, p3], p5], implies[and[p1, p2, p5], p6], 
        not[implies[and[p1, p2, p3], p6]], {p1 -> member[u, x], 
          p2 -> member[pair[u, v], w], 
          p3 -> subclass[w, cart[y, z]], p5 -> member[v, z], 
          p6 -> member[v, image[w, x]]}]]

or[member[v_, image[w_, x_]], not[member[u_, x_]], 
        not[member[pair[u_, v_], w_]], not[subclass[w_, cart[y_, z_]]]] := 
      True

two results related to Quaife's theorem (IM5)

Lemma.

SubstTest[implies, subclass[u, y], subclass[image[x, u], image[x, y]], 
      u -> domain[x]]

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

Theorem IM-5B, a corollary of Quaife's theorem (IM5) proved 1997 July 24 using Otter, resembles this lemma, but with  equal  replacing  subclass in the conclusion:

or[not[subclass[domain[x], y]], equal[range[x], image[x, y]]] // 
      AssertTest

or[equal[image[x_, y_], range[x_]], not[subclass[domain[x_], y_]]] := 
      True

Theorem IM-5C, another corollary of Quaife's theorem (IM5)  also proved 1997 July 24 using Otter  is a variant of the above.  Here is a slightly more general result:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], {p1 -> subclass[x, cart[y, z]], 
          p2 -> subclass[domain[x], y], 
          p3 -> equal[image[x, y], range[x]]}]]

or[equal[image[x_, y_], range[x_]], not[subclass[x_, cart[y_, z_]]]] := 
      True

a curiosity

Theorem IM-SU-V, a curious result proved 1998 April 21using Otter, is transformed as follows by the GOEDEL program:

subclass[image[x, y], image[V, x]]

Its truth can be established as follows:

SubstTest[implies, equal[y, z], 
      equal[image[w, y], image[w, z]], {z -> 0, 
        w -> composite[id[x], FIRST]}]

or[equal[0, intersection[x_, domain[y_]]], not[equal[0, y_]]] := 
      True