Next: Herbrand
Hilbert gave the following courses on logic and foundations
in the period 1917-1922:
He received considerable help in the preparation and eventual write up of these lectures from Bernays. This material was subsequently reworked by Ackermann into the book Principles of Theoretical Logic (1928) by Hilbert and Ackermann. The book was intended as an introduction to mathematical logic, and to the forthcoming book of Hilbert and Bernays (dedicated essentially to the study of first-order number theory). In 120 pages they cover:
Let us make a few comments about each of these chapters.
Chapter I discusses the basic connectives , , , , (they use the notation &, , , , ), the commutative, associative and distributive laws, and reducing the number of connectives needed. They say (p. 9):
As a curiosity let it be noted that one can get by with a single logical sign, as Sheffer showed.
This is closer to the importance now attached to Sheffer's discovery than Whitehead and Russell's statement in the second edition of Principia Mathematica that Sheffer's reduction of the propositional logic to a single binary connective was the most important development in logic since their first edition had appeared. Indeed Whitehead and Russell added the necessary text to Principia to reduce their development, based on and , to the Sheffer stroke.
Next Hilbert and Ackermann show how to put propositions in conjunctive, or disjunctive, normal form, and show how one can use this to describe all the consequences of a finite set of propositions. Then they discuss how one determines if a statement is a tautology (they say universally valid), or satisfiable.
They follow Principia in the axiomatization of the propositional calculus, using the work of Bernays (1926) to reduce the list of axioms from 5 to 4. Turning to the questions associated with the axiomatic method (Theoretical Logic, p. 29) they say:
The most important of the questions which arise are those of , , and .
After noting that one can derive precisely the tautologies in their system, the solutions of these questions for this propositional calculus, due to Bernays (1926), are presented. The completeness result is the strong version, namely that adding any non-tautology to the axioms permits the derivation of a contradiction, and hence the derivation of all propositional formulas.
The brief treatment of the calculus of classes in Chapter II is actually a nonaxiomatic version of the first-order logic of unary predicates, a system which is considerably more expressive than the traditional calculus of classes, and in which one can formulate Aristotle's syllogisms.
Chapter III starts off with a famous quote of Kant:
It is noteworthy that till now it [logic] has not been able to take a single step forward [beyond Aristotle], and thus to all appearances seems to be closed and compete.
Then they say about the logic of Aristotle:
It fails everywhere that it comes to giving a symbolic representation to a relation between several objects .
and that such a situation (Theoretical Logic, p. 44):
exists in almost all complicated judgements.
The first-order system they develop uses relations and constant symbols, but equality is not a part of the logic. Furthermore, their relations are many-sorted, both in their examples and formalized logic (Theoretical Logic, pp. 45, 53, 70). In the second edition (1937) the formal version is one-sorted, but the examples are still many-sorted; and a technique using unary domain predicates for converting from many-sorted to one-sorted is given (Theoretical Logic, p. 105).
As one example of how to express mathematics in their formal system they turn to (one-sorted) natural numbers, using two binary relation symbols = and F (for successor) and the constant symbol 1, and write out three properties:
Their formal system is the following:
6. Axioms:
.
7. Rules of Inference:
(provided x is not free in )
The simple form of the last two axioms and the last rule of inference was due to Bernays. Using this system they show elementary facts, such as every formula can be put in prenex form.
Then they turn to the questions that they have designated as important. Using a one-element universe they show the above axiom system is consistent (recall Frege's system was not consistent). Then they say (Theoretical Logic, p. 65):
With this we have absolutely no guarantee that the introduction of assumptions, in symbolic form, to whose interpretation there is no objection, keeps the system of derivable formulas consistent. For example, there is the unanswered question of whether the addition of the axioms of mathematics to our calculus leads to the provability of every formula. The difficulty of this problem, whose solution has a central significance for mathematics, is in no way comparable to that of the problem just handled by us . To successfully mount an attack on this problem, D. Hilbert has developed a special theory.
Ackermann's proof that the above system is not complete in the stronger sense is given (Theoretical Logic, pp. 66-68), namely they show and its negation are not derivable. Then the following is said (Theoretical Logic, p. 68):
It is still an unsolved problem as to whether the axiom system is complete in the sense that all logical formulas which are valid in every domain can be derived. It can only be stated on empirical grounds that this axiom system has always been adequate in the applications. The independence of the axioms has not been investigated.
After some examples of using this system, they turn to the decision problem in §11 of Chapter III. We quote (Theoretical Logic, p. 72):
According to the methods characterized by the last examples one can apply the first-order calculus in particular to the axiomatic treatment of theories .Once logical formalism is established one can expect that a systematic, so-to-say computational treatment of logical formulas is possible, which would somewhat correspond to the theory of equations in algebra.
We met a well-developed in the propositional calculus. The most important problems solved there were the and of a logical expression. Both problems are called the .
(Theoretical Logic, p. 73)
The two problems are dual to each other. If an expression is not universally valid then its negation is satisfiable, and conversely.The decision problem for first-order logic now presents itself . One can restrict oneself to the case where the propositional variables do not appear .
The decision problem is solved if one knows a process which, given a logical expression, permits the determination of its validity resp. satisfiability.
The solution of the decision problem is of fundamental importance for the theory of all subjects whose theorems are capable of being logically derived from finitely many axioms .
(Theoretical Logic, p. 74)
We want to make it clear that for the solution of the decision problem a process would be given by which nonderivability can, in principle, be determined, even though the difficulties of the process would make practical use illusory .
(Theoretical Logic, p. 77)
the decision problem be designated as the main problem of mathematical logic.in first-order logic the discovery of a general decision procedure is still a difficult unsolved problem .
In the last section of Chapter III they give Löwenheim's decision procedure for first-order statements involving only unary relation symbols, namely one shows that it suffices to examine all domains of size less than or equal to , where k is the number of unary predicate symbols in the statement. Consequently (p. 80)
...postulating the validity resp. satisfiability of a logical statement is equivalent to a statement about the size of the domain.One can also pose the simpler problem of when a given expressionIn the most general sense one can say the decision problem is solved if one has a procedure that determines for each logical expression for which domains it is valid resp. satisfiable.
is valid for all domainsand when not. This would suffice, with the help of the decision process, to answer whether a given statement of an axiomatically based subject was provable from the axioms.
Then they point out that one cannot hope for a process based on examining finite domains, as in the unary predicate calculus; but that Löwenheim's theorem gives a strong analog, namely a statement is valid in all domains iff it is valid in a countably infinite domain. Then they attempt to tie the decision problem to the completeness problem (Theoretical Logic, p. 80):
Examples of formulas which are valid in every domain are those derived from the predicate calculus. Since one suspects that this system gives all such [valid] formulas, one would move closer to the solution of the decision problem with a characterization of the formulas provable in the system.A general solution of the decision problem, whether in the first or second formulation, has not appeared till now. Special cases of the decision problem have been attacked and solved by P. Bernays, and M. Schoenfinkel, as well as W. Ackermann.
Finally they note that Löwenheim showed one could restrict ones attention to unary and binary predicates.
Chapter IV starts out by trying to show that one needs to extend first-order logic to handle basic mathematical concepts. The extension takes place by allowing quantification of relation symbols. Then one can express complete induction by (Theoretical Logic, p. 83):
or, to be more explicit,
one can put the universal quantifier (P) in front of the formula.Identity between x and y, , is defined by .
Then they say (Theoretical Logic, p. 86):
The solution of this general decision problem (for the extended logic) would not only permit us to answer questions about the provability of simple geometric theorems, but it would also, at least in principle, make possible the decision about the provability, resp. nonprovability, of an arbitrary mathematical statement.The first-order calculus was fine for a few special theories,
But as soon as one makes the foundations of theories, especially of mathematical theories, as the object of investigation the extended calculus is indispensable.The first important application of the extended calculus is to numbers. Individual numbers are realized as properties of predicates, e.g.,
The condition for being a [cardinal] number is
where SC (F,G) says there is a 1-to-1 correspondence between the elements satisfying F and those satisfying G. Having set up the definitions and assuming an infinite domain, they say (footnoting Whitehead and Russell) that:
It is also of particular interest that the number theoretic axioms become logically provable theorems.They develop set theory in this extended calculus by saying that sets are the extension of unary predicates; thus two predicates F and G determine the same set iff holds, which is abbreviated to Aeq (F,G). Then properties of sets correspond to unary predicates P of unary predicates, where P is invariant under Aeq. Sets of ordered pairs correspond to binary predicates, etc. Under this translation a number becomes a set of sets of individuals from the domain, namely a number is the set of all sets equivalent to a given set. Their development of set theory ends with union, intersection, ordered sets and well-ordered sets defined, and they say that all the usual concepts of set theory can be expressed symbolically in their system.
Having shown the expressive power of the extended calculus of relations they turn to the problem of finding axioms and rules of inference. Obvious generalizations from the first-order logic lead to contradictions through the well-known paradoxes. Finally they outline Whitehead and Russell's ramified theory of types (with its questionable axiom of reducibility) which allows one to give axioms and rules of inference generalizing those of the first-order, avoiding the usual encoding of the paradoxes as contradictions, and being strong enough to carry out traditional mathematics. After mentioning that the decision problem also applies to the system of Principia, the book closes with Hilbert claiming to have a development of extended logic, which will soon appear, which avoids the difficulties of the axiom of reducibility.
Looking back over this book we see that its purpose is to present formal systems, and give examples. There are almost no real theorems of mathematical logic proved, or stated, after the development of the propositional calculus in Chapter I; the main exceptions being a proof of Löwenheim's decision process for the first-order unary relational logic, and the statement of the Löwenheim-Skolem theorem. First-order set theory is not even mentioned.
Next: Herbrand
Fri Jan 31 14:07:53 EST 1997