Logic II for Mathematicians and Computer Scientists

Date and Time

Tuesday, 13:00 - 14:30, TNF 416 Start: 9.3.

Lecture notes are now available in dvi format and postscript format.

Since communication skills become more and more important for mathematicians and computer scientists, it is a dedicated goal of the lecture to learn and practice oral presentations of difficult proofs in logic. Therefore, it is planned that a large portion of the material is presented by participants.

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 second aspect into account, we will in particular focus on algorithmic theorems and theoretical foundations of automated theorem proving. In order to take the first aspect into account, we will restrict metatheory to finitary methods, except in our discussion of the completeness theorem where this is not possible.

Predicate calculus

(also called first order logic). We give proofs for Church's result of undecidability of predicate calculus, Gödel's completeness theorem, and Herbrand's theorem.

Formal analysis

. We give an axiomatization of the first order theory of the real numbers and the decidability due to Tarski. As an application, we give an axiomatization of geometry (also due to Tarski), which is also decidable. In contrast to this, we discuss constructive analysis in an informal way.

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.