Some difficulties arise from each of these points of style. The
solutions to these difficulties, and even the precise nature of the
difficulties themselves, are best appreciated by examining the theory
*EFT* (``external function theory'') which was implemented in
the original version of this theorem prover (the following is
excerpted from an unpublished paper).

*EFT* is an equational theory. There are two (apparent) sorts,
called objects and Functions. Object variables and constants will
begin with lower-case letters; Function variables and constants will
begin with upper-case letters. The ``intended interpretation" is that
the objects are the elements of some infinite set and the Functions
are the functions from that set into itself (or a subset of the
collection of such functions closed under certain operations). But
see below for an alternate interpretation.

*t* and *f* are distinct atomic object constants (used to represent
the truth values). If *x* and *y* are object terms, (*x*,*y*) is an
object term, the ordered pair with projections *x* and *y*. If *F* is
a Function term and *x* is an object term, *F*[*x*] is an object term,
the value of *F* at *x* or the result of application of *F* to *x*.
Cond and Id are atomic Function terms. Id is intended to be the
identity function; Cond[(*x*,*y*),(*z*,*w*)] is intended to be *z* if *x* =
*y*, *w* otherwise. If *x* is an object term, |*x*| is a Function term,
the constant Function of *x*. If *F* and *G* are Function terms,
(*F*,*G*) is a Function term, the product of *F* and *G*, and
is a Function term, the composition of *F* and *G*.
If *F* is a Function term, *F*! is a Function, called the ``Hilbert
Function" of *F*. *F*![*y*] is intended to be an object such that
*F*[*F*![*y*],*y*] is not *t*, if there is any such object; its value is a
matter of indifference otherwise. We write *F*[*x*,*y*],
, instead of *F*[(*x*,*y*)], ,
respectively. We define the *n*-tuple
inductively as . Sentences of *EFT*
are equations between object terms. The rules of *EFT* enable
substitutions of equals for equals:

**A.**- Reflexivity, symmetry, transitivity of equality.
**B.**- If
*a*=*c*,*b*=*d*are theorems, (*a*,*b*) = (*c*,*d*) is a theorem. **C.**- If
*a*=*b*is a theorem,*F*[*a*] =*F*[*b*] is a theorem. **D.**- Uniform substitution of an object term for an object
variable or of a Function term for a Function variable in a theorem yields a theorem.

Note that the rules do not directly permit substitutions of equals for equals where object terms appear as subterms of Function terms. The axioms are as follows:

**(CONST)**- |
*x*|[*y*] =*x* **(ID)**- Id[
*x*] =*x* **(PROD)**- (
*F*,*G*)[*x*] = (*F*[*x*],*G*[*x*]) **(COMP)****(PROJ1)**- Cond[(
*x*,*x*),(*y*,*z*)] =*y* **(PROJ2)**- Cond[(
*t*,*f*),(*y*,*z*)] =*z* **(DIST)**-
*F*[Cond[(*x*,*y*),(*z*,*w*)] = Cond[(*x*,*y*),(*F*[*z*],*F*[*w*])] **(HYP)**- Cond[(
*x*,*y*),(*F*[*x*],*z*)] = Cond[(*x*,*y*),(*F*[*y*],*z*)] **(HILBERT)**- Cond[(
*F*[*F*![*y*],*y*],*t*),(*F*[*x*,*y*],*t*)] =*t*

It should be clear that the axioms are true in the intended interpretation (under the Axiom of Choice), and they should also serve to clarify the exact interpretations of the term constructions. If a version of the ``intended interpretation" with a restricted class of functions interpreting the Functions of the theory is to be constructed, the axioms indicate the set of operations under which the restricted class of functions needs to be closed.

We have the following Abstraction Theorem:

**Theorem:**- If
*s*is an object term and*x*is an object variable which does not appear as a subterm of any Function subterm of*s*, there is a function term such that*x*does not appear as a subterm of and ``" is a theorem. **Proof:**- By induction on the structure of terms. If
*s*is*x*, is Id; if*s*is an atom*a*distinct from*x*, is |*a*|. If*s*is of the form (*u*,*v*), . If*s*is of the form*U*[*v*],*U*does not involve*x*and .

such that ``" is a theorem can be
defined as , where *z* is a variable not appearing in *s* and
is the result of replacing *x* with Cond[(*t*,*t*),*z*] and *y* with
Cond[(*t*,*f*),*z*] wherever they appear in *s*. Cond[(*t*,*t*),*z*]) and Cond[(*t*,*f*),*z*]) are the
projection Functions and .

An interesting point about abstracts constructed following the proof
of the Theorem is that they resemble the term from which they are
abstracted in structure. This helps to make *EFT* an
environment in which it is practical to avoid the use of bound
variables.

Fri Sep 5 16:28:58 MDT 1997