next up previous
Next: Conclusion: Mathematical Theory of Up: Relation to Other Formalisms Previous: Recursive function theory

On the Relations between Computation and Mathematical Logic

 

In what follows computation and mathematical logic will each be taken in a wide sense. The subject of computation is essentially that of artificial intelligence since the development of computation is in the direction of making machines carry out ever more complex and sophisticated processes, i.e. to behave as intelligently as possible. Mathematical logic is concerned with formal languages, with the representation of information of various mathematical and non-mathematical kinds in formal systems, with relations of logical dependence, and with the process of deduction.

In discussions of relations between logic and computation there has been a tendency to make confused statements, e.g. to say that aspect A of logic is identical with aspect B of computation, when actually there is a relation but not an identity. We shall try to be precise.

There is no single relationship between logic and computation which dominates the others. Here is a list of some of the more important relationships.

1. Morphological parallels

The formal command languages in which procedures are described, e.g. ALGOL; the formal languages of mathematical logic, e.g. first order predicate calculus; and natural languages to some extent: all may be described morphologically (i.e., one can describe what a Grammatical sentence is) using similar syntactical terms. In my opinion, the importance of this relationship has been exaggerated, because as soon as one goes into what the sentences mean the parallelism disappears.

2. Equivalent classes of problems

Certain classes of problems about computations are equivalent to certain classes of problems about formal systems. For example, let E tex2html_wrap_inline2009 be the class of Turing machines with initial tapes,

E tex2html_wrap_inline2011 be the class of formulas of the first order predicate calculus,

E tex2html_wrap_inline2013 be the class of general recursive functions,

E tex2html_wrap_inline2015 be the class of formulas in a universal Post canonical system,

E tex2html_wrap_inline2017 be a class of each element which is a Lisp S-function f together with a suitable set of arguments tex2html_wrap_inline2021

E tex2html_wrap_inline2023 be a program for a stored program digital computer.

About E tex2html_wrap_inline2009 we ask: Will the machine ever stop?

About E tex2html_wrap_inline2011 we ask: Is the formula valid?

About E tex2html_wrap_inline2013 we ask: Is f(0) defined?

About E tex2html_wrap_inline2015 we ask: Is the formula a theorem?

About E tex2html_wrap_inline2017 we ask: Is tex2html_wrap_inline2037 defined?

About E tex2html_wrap_inline2023 we ask: Will the program ever stop?

For any pair (E tex2html_wrap_inline2041 ,E tex2html_wrap_inline2043 ) we can define a computable map that takes any one of the problems about elements of E tex2html_wrap_inline2041 into a corresponding problem about an element of E tex2html_wrap_inline2041 and which is such that the problems have the same answer. Thus, for any Turing machine and initial tape we can find a corresponding formula of the first order predicate calculus such that the Turing machine will eventually stop if and only if the formula is valid.

In the case of E tex2html_wrap_inline2023 if we want strict equivalence the computer must be provided with an infinite memory of some kind. Practically, any present computer has so many states, e.g. tex2html_wrap_inline2051 , that we cannot reason from finiteness that a computation will terminate or repeat before the solar system comes to an end and one is forced to consider problems concerning actual computers by methods appropriate to machines with an infinite number of states.

These results owe much of their importance to the fact that each of the problem classes is unsolvable in the sense that for each class there is no machine which will solve all the problems in the class. This result can most easily be proved for certain classes (traditionally Turing machine), and then the equivalence permits its extension to other classes. These results have been generalized in various ways. There is the world of Post, Myhill, and others, on creative sets and the work of Kleene on hierarchies of unsolvability. Some of this world is of potential interest for computation even though the generation of new unsolvable classes of problems does not in itself seem to be of great interest for computation.

3. Proof procedures and proof checking procedures

The next relation stems from the fact that computers can be used to carry out the algorithms that are being devised to generate proofs of sentences in various formal systems. These formal systems may have any subject matter of interest in mathematics, in science, or concerning the relation of an intelligent computer program to its environment. The formal system on which the most work has been done is the first order predicate calculus which is particularly important for several reasons. First, many subjects of interest can be axiomatized within this calculus. Second, it is complete, i.e. every valid formula has a proof. Third, although it seems unlikely that the general methods for the first order predicate calculus will be able to produce proofs of significant results in the part of arithmetic axiomatizable in this calculus (or in any other important domain of mathematics), the development of these general methods will provide a measure of what must be left to subject-matter-dependent heuristics. It should be understood by the reader that the first order predicate calculus is undecidable; hence there is no possibility of a program that will decide whether a formula is valid. All that can be done is to construct programs that will decide some cases and will eventually prove any valid formula but which will run on indefinitely in the case of certain invalid formulas.

Proof-checking by computer may be as important as proof generation. It is part of the definition of formal system that proofs be machine checkable. In my forthcoming paper [9], I explore the possibilities and applications of machine checked proofs. Because a machine can be asked to do much more work in checking a proof than can a human, proofs can be made much easier to write in such systems. In particular, proofs can contain a request for the machine to explore a tree of possibilities for a conventional proof. The potential applications for computer-checked proofs are very large. For example, instead of trying out computer programs on test cases until they are debugged, one should prove that they have the desired properties.

Incidentally, it is desirable in this work to use a mildly more general concept of formal system. Namely, a formal system consists of a computable predicate

displaymath2053

of the symbolic expressions statement and Proof. We say that Proof is a proof of statement provided

displaymath2053

has the value T.

The usefulness of computer checked proofs depends both on the development of types of formal systems in which proofs are easy to write and on the formalization of interesting subject domains. It should be remembered that the formal systems so far developed by logicians have heretofore quite properly had as their objective that it should be convenient to prove metatheorems about the systems rather than that it be convenient to prove theorems in the systems.

4. Use of formal systems by computer programs

When one instructs a computer to perform a task one uses a sequence of imperative sentences. On the other hand, when one instructs a human being to perform a task one uses mainly declarative sentences describing the situation in which he is to act. A single imperative sentence is then frequently sufficient.

The ability to instruct a person in this way depends on his possession of common-sense which we shall define as the fact that we can count on his having available any sufficiently immediate consequence of what we tell him and what we can presume he already knows. In my paper [10] I proposed a computer program called the Advice Taker that would have these capabilities and discussed its advantages. The main problem in realizing the Advice Taker has been devising suitable formal languages covering the subject matter about which we want the program to think.

This experience and others has led me to the conclusion that mathematical linguists are making a serious mistake in their almost exclusive concentration on the syntax and, even more specially, the grammar of natural languages. It is even more important to develop a mathematical understanding and a formalization of the kinds of information conveyed in natural language.


next up previous
Next: Conclusion: Mathematical Theory of Up: Relation to Other Formalisms Previous: Recursive function theory

John McCarthy
Wed May 1 20:03:21 PDT 1996