Theorem Proving in Type Theory

THEOREM PROVING IN TYPE THEORY

Peter B. Andrews and Eve Longini Cohen Mathematics Department Carnegie- Mellon University Pittsburgh, Pennsylvania 15213

As one aspect of the endeavor to cre­ ate new intellectual tools for mankind, we wish to enable computers to prove, and to assist in the proofs of, theorems of mathematics and (eventually) other disci­ plines which have achieved the requisite logical precision . For this purpose, a particularly suitable formal language is Church's formulation [4] of type theory with A-conversion. In this language tra­ ditional mathematical notations can be expressed very directly, and the intui­ tive distinctions between different types o f mathematical entities (such as num­ bers , functions , and sets of functions) are made syntactically explicit .

The program for proving theorems of type theory which we discuss is intended to provide experience relevant to such a project , and was developed with the aid of Charles E. Blair and John J.

Grefenstette.

After reducing the negation of the sentence to be proved to a set of clauses (basically as in the resolution method) , the program seeks an acceptable mating by the method outlined in [3] . The unifying substitutions are found by Huet's algo­ rithm [6] , augmented by heuristics to minimize branching of the search tree, and a procedure for deleting nodes which are essentially supersets of other nodes. The semi-decision procedures which search for a potentially acceptable mating and for the associated unifying substitutions operate in parallel , and interact so that information acquired by each procedure limits the other's search . After an acceptable mating is found , the computer constructs from it a more traditional refutation, using substitution, cut (ground resolution) , and simplification of disjunctions as rules of inference .

The program can be run in automatic or interactive mode. The interactive sys­ tem embodies a set of logical rules which is in a certain sense complete [1] , but the user must provide some of the substi­ tutions for predicate variables. (As shown in [2] , even completeness in this weak sense is not trivial.) The program in automatic mode is not logically com­ plete for type theory (though it is com­ plete when applied to sentences of first

This research was supported by NSF Grants DCR71-0l953-A04 and MCS76-06087 .

order logic) , since no practical method is known for automatically generating all required substitutions for predicate var­ iables. This is the fundamental theoreti­ cal problem of automatic theorem-proving in type theory, and no practical general solution to it seems imminent, since sub­ stitutions for predicate variables often express the important concepts in a mathematical proof.

As noted in [1] , for certain purposes axioms of extensionality, descriptions, or choice must be taken as hypotheses. Actually , the introduction of Skolem functions to eliminate essentially exis­ tential quantifiers involves an implicit use of the Axiom of Choice (AC) in type theory , so the system can prove certain consequences of AC , such as

1fY 1 :az 1 [R 011 Y 1 Z 1 ] ::l :3:F 11 1fY 1 [R 011 Y 1 [F 11 Y 1 ]] ·

Among the theorems which can be proved completely automatically are Can­ tor's Theorems that a set . has more sub­ sets than members , and that there are more functions on a non-unit set than members of the set. (Thus there are un­ countably many functions of natural num­ bers . ) Following [5] , the Cantor Theorem for Sets can be expressed by the sentence -:3:H 011 1fS 01 :3:J 1 [H 011 J 1 = S 01 ], which asserts that there is no function H from individuals to sets which has every set S in its range. The computer decides to substitute for S the wff 01

[AX, . - H 011 X 1 X 1 ] , which denotes the set (x J- X E Hx}, and expresses the key i dea in the classical diagonal argument.