next up previous contents
Next: Implementation of EFT Up: Logical Style Previous: The Main Points

The Logic of an Old Version

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.


next up previous contents
Next: Implementation of EFT Up: Logical Style Previous: The Main Points

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997