Quaife's Theorem (LD8)

Johan G. F. Belinfante and Ming Li
2007 April 7

SetDirectory["l:"];  << goedel92.05b; << tools.m

summary

Quaife's theorem (LD8) says that linear differences are (almost) symmetric.  If z is a linear difference of x and y, and if y is nonzero, then z is also a linear difference of y and x.

"Art Quaife, Automated Development of Fundamental Mathematical \
Theories, Appendix 3. Theorems Proved in Peano's Arithmetic, Kluwer Academic \
Publishers, Dordrecht, 1992. Cf. p. 201";

In the course of proving that any linear difference sets is the set of multiples of some natural number, the following variant of this theorem was derived, with nat wrappers on the variables x and y, and the third variable z eliminated.

or[equal[0, nat[y]], 
      subclass[ld[nat[x], nat[y]], ld[nat[y], nat[x]]]]

In this notebook a wrapper-free version of this theorem is derived, and the variable z is restored to enable Quaife's original statement to be more closely approximated.

derivation

Lemma.

SubstTest[implies, equal[0, t], subclass[t, ld[y, x]], 
        t -> ld[x, y]] // Reverse

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

Lemma.

SubstTest[implies, and[equal[x, nat[u]], equal[y, nat[v]]], 
        or[equal[0, y], subclass[ld[x, y], ld[y, x]]], {u -> x, 
          v -> y}] // Reverse

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

Theorem.   (Wrapper-free version of a theorem currently in the GOEDEL program.  That rule can be replaced with this new one.)

SubstTest[and, implies[p, q], 
      or[p, q], {p -> and[member[x, omega], member[y, omega]], 
        q -> or[equal[0, y], subclass[ld[x, y], ld[y, x]]]}]

or[equal[0, y_], subclass[ld[x_, y_], ld[y_, x_]]] := True

Introducing a variable yields this corollary that more closely resembles Quaife's clause (LD8).

SubstTest[implies, and[member[z, u], subclass[u, v]], 
        member[z, v], {u -> intersection[image[V, y], ld[x, y]], 
          v -> ld[y, x]}] // Reverse

or[equal[0, y_], member[z_, ld[y_, x_]], not[member[z_, ld[x_, y_]]]] := 
      True