Davis_and_Putnam__1960__A_Computing_Procedure_for_Quantification_Theory.pdf

|
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
 18 views
of 15

Please download to get full document.

View again

Description
A Computing Procedure for Quantification Theory* ~RTIiN D~_v~s Rensselaer Polytechnic Institute, Hartford Division, East Windsor Hill, Conn. AND HILARY PUTNAM' Princeton University, Princeton, New Jersey The hope that mathematical methods employed in the investigation of formal logic would lead to purely computational methods for obtaining mathematica
Share
Tags
Transcript
  A Computing Procedure for Quantification Theory* ~RTIiN ~_v~s Rensselaer Polytechnic Institute, Hartford Division, East Windsor Hill, Conn. AND HILARY PUTNAM' Princeton University, Princeton, New Jersey The hope that mathematical methods employed in the investigation of formal logic would lead to purely computational methods for obtaining mathematical theorems goes back to Leibniz and has been revived by Peano around the turn of the century and by Hilbert's school in the 1920%. Hilbert, noting that all of classical mathematics could be formalized within quantification theory, declared that the problem of finding an algorithm for determining whether or not a given formula of quantification theory is valid was the central problem of mathe- matical logic. And indeed, at one time it seemed as if investigations of this de- cision problem were on the verge of success. However, it was shown by Church and by Turing that such an algorithm can not exist. This result led to consider- able pessimism regarding the possibility of using modern digital computers in deciding significant mathematical questions. However, recently there has been a revival of interest in the whole question. Specifically, it has been realized that while no decision procedure exists for quantification theory there are many proof procedures available--that is, uniform procedures which will ultimately locate a proof for any formulai of quantification theory which is valid but which will usually involve seeking forever in the Case of a formula which is not valid-- and that some of these proof procedures could well turn out to be feasible for use with modern computing machinery. Hao Wang [9] and P. C. Gilmore [3] have each produced wor]dng programs which employ proof procedures in quantification theory. Gilmore's program employs a form of a basic theorem of mathematical logic due to Herbrand, and Wang's makes use of a formulation of quantification theory related to those studied by Gentzen. However, both programs encounter decisive difficulties with any but the simplest formulas of quantification theory, in connection with methods of doing propositional calculus. Wang's program, because of its use of Gentzen-like methods, involves exponentiation on the total number of truth- functional connectives, whereas Gilmore's program, using normal forms, in- volves exponentiation on the number of clauses present. Both methods are su- perior in many cases to truth table methods which involve exponentiation on the * Received September, 1959. This research was supported by the United States Air Force through the Air Force Office of Scientific Research of the Air Research and Develop- ment Command, under Contract No. AF 49(638)-527. Reproduction in whole or in part is permitted for any purpose of the United States Government. 201  202 M. DAVIS AND H. PUTNAM total number of variables present, and represent important initial contributions, but both run into difficulty with some fairly simple examples. In the present paper, a uniform proof procedure for quantification theory is given which is feasible for use with some rather complicated formulas and which does not ordinarily lead to exponentiation. The superiority of the present pro- cedure over those previously available is indicated in part by the fact that a formula on which Gilmore's routine for the IBM 704 causes the machine to compute for 21 minutes without obtaining a result was worked successfully by hand computation using the present method in 30 minutes. Cf. §6, below. It should be mentioned that, before it can be hoped to employ proof procedures for quantification theory in obtaining proofs of theorems belonging to genuine mathematics, ~nlte axiomatizations, which are short, must be obtained for various branches of mathematics. This last question will not be pursued further here; cf., however, Davis and Putnam [2], where one solution to this problem is given for elementary number theory. 1. General Remarks We shall describe a computational procedure, or algorithm, which when ap- plied to a logically valid formula written in the notation described below will terminate and yield a proof Of the validity of that formula; for formulas which are not logically valid, the computation will continue indefinitely without giving a result: The symbols of which our formulas are constructed are divided into the classes: punctuation marks, logical symbols, (individual) variables, predicate symbols, and function symbols. The punctuation marks are: , ) The logical symbols are: & Y --~ ~-~ E We shall take as the variables the terms of the following infinite sequence: x~ x2 xs x4 ..- The predicate symbols will be the letters F, G, H, with or without subscripts, and the function symbols 2 will be the terms of the infinite sequence: Among all of the expressions (e.g. ~ V Fx~E) which can be formed using these symbols, we distinguish three classes: the terms, the atomic formulas, and the well-formed formulas (abbreviated w.f f ). 1 Since by results of Church and Turing the set of formulas involved is a recursively enumerable set which is not recursive (for terminology, and a proof of this fact, of. [1] or [6]), this kind of algorithm is the best one can hope to obtain. 2 We intend to use function symbols not only to stand for functions of one or more argu- ments but also for individuals. In the latter use they may be thought of as standing for functions of zero argument.  A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY 203 The notion term will be defined inductively: (1) The expressions f~ and x, are terms for each i = 1, 2, 3, .... (2) If pl , p2 , , pn are terms,a then so is f~(pl , p2 , , p~), and pl , p2 , , p,~ are called the arguments of f ~. (3) The terms consist exactly of the expressions generated by (1) and (2). Next: The expression p(pl, p2, , pn) is an atomic formula if p is a predicate symbol and pl , p2, ã ã ã , pn are terms, pl , p2 , ã ã ã , pn are called the arguments of p. Finally: (1) An atomic formula is a wJJ. (2) If R is a w.f.f., then so are ,-~R, (x,)R, and (Ex~)R. (3) If R and S are w.f.f.'s, then so are (R & S), (R Y S), (R ~ S), and R We introduce the following abbreviative conventions: a stands for f~. f stands for f2. pq stands for p(q) if p is a function symbol and q is a term. ~(pl, p2, ' , pn) stands for -~p(pl, , pn), where p is a predicate symbol and p~, .. ã , p~ are terms. An occurrence of x~ in a w.f.f. R is a bound occurrence if it is in a w.f. part of R of the form (x,)P or (Ex,)P. An occurrence of x, which is not bound is called a free occurrence, x, is free in R if it has at least one flee occurrence in R. If x~, x~, .-., x~ are all of the free variables in R, we sometimes write R(x~, x~2, , x,,,) for R. If pl, p2, -- , p~ are terms, we write R(pl, p~, ã . ã , p~) for the result of replacing x~ by pk, /c = 1, 2, .. ã , n, at all free oc- currences of x~k in R. Parentheses will be omitted wherever their omission can cause no confusion. Our next step is to single out from the class of w.f.f.'s those which are logically valid. This can be done either by specifying axioms and rules of inference or by referring to interpretations of the w.f.f.'s of the system, and by a basic result due to GSdel 4 both of these procedures will lead to the same class of formulas. For our present purposes it is most convenient to use the latter formulation em- ploying interpretations. An interpretation for a formula R consists of a nonempty set of elements U called a universe and an assignment of values to each function symbol and predicate symbol as follows: To each function symbol which occurs in R with n arguments, 5 we assign a function of n variables ranging over U, whose values are in U. e To each predicate symbol which occurs in R with n arguments, we assign a 3 Note that the symbols p~, p~, etc. occur here as syntactic variables. That is, they stand for expressions made up of our symbols. 4 The GSdel completeness theorem. Cf. [5], [6], or [7]. Thus, if n -- 0, ]~ is assigned an element of U. 6 Note that if f~ occurs in R both with m arguments and with n arguments, m ~ n, it is assigned different functions in each case. In practice this will not happen in examples con- sidered below. (However, two occurrences in R of f~ with the same number of arguments are, of course, to be assigned the same value.)  20,~ M. DAVIS A.i~D H. PUTNAM function of n variables ranging over U, whose values are the truth values, 0 (falsehood) and 1 (truth)/ Let R(xnl, x~, -.. , xn~) be a w.f.f. Then, given an interpretation of R over universe U, the value 0 or 1 will be assigned to R(tl, t2, ã ã , t~) for each ordered k-tuplet (tl, h, ' , tk) of elements of U. This value may be obtained simply by interpreting 0 as falsehood and 1 as truth, using the usual truth tables for ~ & y ~ and ¢-~, interpreting (x~)P(x~) as 0 unless P(t) has the value 1 for all t in U, and interpreting (Ex~)P(x~) as 1 unless P(t) has the value 0 for all t in U. A w.f.f. R is called valid if under every interpretation and for every set of argu- ments from U, R is assigned the value 1. A w.f.f. R is called consistent (or satisfiable) if there is some interpretation under which R is assigned the value 1, for some choice of arguments from U. R is inconsistent if it is not consistent. We shall make use of the obvious fact that: R is valid if and only if NR is inconsistent. That is, to prove R it sill ices to refute ,--~R, and indeed our proof procedure for validity will be couched in the form of a refutation procedure. R is called logically equivalent to S if the w.f.f. (R ~ S) is valid. A w.f.f, is called quantifier-free if it contains no occurrence of (x~) or (Ex~). A w.f.f, is a prenex formula, or in prenex normal form, if it begins with a sequence of quantifiers (x~) and (Ex~) in which no variable occurs more than once (called the prefix) and if the sequence is followed by a quantifier free w.f.f. (called the matrix). An example of a prenex formula is: (xl) (Ex3) (xT) (Ex~)r(f(x~), f3(xl , x~), xs) S is called a prenex normal form of R if S is a prenex formula which is logically equivalent to R. There is a simple algorithm (cf. [5], [7]), for obtaining a prenex normal form of a given w.f.f. Thus, for the purpose of our refutation procedure it su~ces to consider prenex formulas. The disjunction of R~,...,R., n=> 1, is the w.f.f. R~ Y R2 V ..- Y Rn; their conjunction is the w.f.f. R~ & R2 & ... & R~. A literal is a w.f.f, which is either an atomic formula or ~R, where R is atomic. A clause is a disjunction' R~ V R~ Y .. ã V R, in which each R~ is a literal and in which no atomic formula occurs twice. (E.g., F(x~) V G(x~, x3) is a clause, but F(xl) V in(x1) is not.) A conjunction of clauses is said to be a formula in conjunctive normal form. Ex.~PL~: (p Y q V ~) & (s V t)is a formula in conjunctive normal form if p, q, r, s, t are atomic fornmlas. If a w.f.f. A is in conjunctive normal form and A is logically equivalent to B, then A is called a conjunctive normal form of B. EXAMPLE: (p V ~) & (q V p) is a conjunctive normal form of p ~ q if p and q are any atomic formulas. For further discussion of conjunctive normal form the reader may consult Hilbert and Ackermann [5]. In particular, there is a simple algorithm by which T The comment in footnote 6 regarding function symbols applies also to predi- cate symbols.
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks