Logic II for Mathematicians and Computer Scientists

Date and Time

The lecture will be held in two blocks in the week before and after easter holidays.

Schedule:

Tue	24.3.	16:00-19:30	K223B
Thu	26.3.	16:00-19:30	K223B
Fri	27.3.	16:00-19:30	K223B
Tue	31.3.	16:00-19:30	BA9907
Thu	2.4.	16:00-19:30	BA9907
Mon	20.4.	16:00-19:30	K223B
Tue	21.4.	16:00-19:30	K224B

Date of preliminary meeting: Fri 13.3.1998, 10:00, T711.

Version 2 of the lecture notes is now available in dvi format and postscript format. The last two sections are now also available in dvi format and postscript format.

About the Lecture

There are two motivations for the desire to formalize reasoning. On the one hand, one wants to have some sort of "quality control", in order to check and improve reliability and efficiency of proofs. This was the impetus behind Euclid's efforts to formalize geometry. It was also the motivation of Frege, Russell, Hilbert, Dedekind, ..., to construct a universe of mathematics based on formal systems. Historically, the efforts of axiomatization led to the discovery of antinomies, which in turn increased the necessity to improve an reliability. A more modern example are the efforts of Buchberger to improve the "quality of proofs" of his students in his famous Thinking-Speaking-Writing course.

A completely different goal is the desire to automatically generate or verify theorems. This idea can be traced back to Lullus (around 1300, "ars magna") and Leibniz (1646-1716), who distinguishes decision methods "ars iudicandi" and generation methods "ars inveniendi". Modern computer science adopted this vision as the core of the "Artificial Intelligence" program. Even though limitations of this approach became clear, we have now many useful algorithms. Most notably are Robinson's resolution algorithm and Collins' quantifier elimination algorithm.

In order to take the first aspect into account, we will restrict metatheory to finitary methods (as in the textbook of Kleene). In order to take the second aspect into account, we will in particular focus on algorithmic theorems.

Predicate calculus.

(also called first order logic) This part culminates in the completeness proof for Robinson's resolution procedure for semi-decision of predicate formulas. We also give proofs for Church's result of undecidability of predicate calculus, Gödel's completeness theorem, and Herbrand's theorem.

Elementary theory of reals.

We give an axiomatization and discuss the Collins-Tarski decision method. We also give an axiomatization (due to Tarski) of geometry, which is closely related to the elementary theory of reals.

Formal number theory.

Two famous negative results - Gödel's incompleteness theorem and the unsolvability of Hilbert's 10th problem - are obtained as immediate consequences of two positive results (which are closely related): any recursively enumerable set is arithmetic (Gödel) and any recursively enumerable set is diophantine (Matijasevic).

References

 [1]

M. Ben-Or, D. Kozen, and J. H. Reif. The complexity of elementary algebra and geometry. J. Comput. System Sci., 32(2):251-264, 1986.

 [2]

B. Chang and C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

 [3]

G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Lecture Notes In Computer Science, pages 134-183. Springer, 1975. Vol. 33.

 [4]

R. Dedekind. Stetigkeit und irrationale Zahlen. Vieweg, 1872.

 [5]

H. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer, 1983.

 [6]

H. Schwabhäuser and W. Szmielev and A. Tarski. Metamathematische Methoden in der Geometrie. Springer, 1983.

 [7]

A. Heyting. Intuitionism. North-Holland, 1966.

 [8]

D. Hilbert. Grundlagen der Geometrie. Teubner, 1977.

 [9]

D. Hilbert and P. Bernays. Grundlagen der Mathematik I und II. Springer, 1970.

 [10]

T. Jebelean. Automatic theorem proving 1 and 2. Lectures at the university of Linz, winter 1998/99 and summer 1999.

 [11]

A. Jones and Y. Matijasevic. Proof of the recursive unsolvability of hilbert's 10th problem. Am. Math. Monthly, 98:689-709, 1991.

 [12]

S. Kleene. Introduction to Metamathematics. North-Holland, 1967.

 [13]

Y. Manin. A course in mathematical logic. Springer, 1977.

 [14]

A. Margaris. First Order Mathematical Logic. Xerox, 1967.

 [15]

J. Pfalzgraf and D. Wang. Automated practical reasoning. Springer, 1995.

 [16]

J. Renegar. On the computational complexity and geometry of the first-order theory of the reals. Journal of Symbolic Computation, 13(3):255-300, 1992.

 [17]

J. Shoenfield. Mathematical Logic. Addison-Wesley, 1973.

 [18]

R. Smullyan. First order logic. Springer, 1968.

 [19]

A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, second edition, 1951.

 [20]

A. Tarski. What is elementary geometry? In A. Tarski L. Henkin, P. Suppes, editor, Proceedings of an International Symposium on the Axiomatic Method, with Special Reference to Geometry and Physics, Studies in Logic and the Foundations of Mathematics, pages 16-29. Amsterdam: North Holland, 1959.

 [21]

A. Troelstra and D. van Dalen. Constructivism in Mathematics. North-Holland, 1988.