Logic II for Mathematicians and Computer Scientists

RISC-Linz logo

Date and Time

Tuesday, 10:15 - 11:45, TNF 416 Start: 7.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

The objects studied in logics are formal theories. Meta-theory investigates such formal calculi from a combinatorial point of view. In model theory, the relation between the formal theory and its semantic is investigated. In this lecture, we discuss selected topics from these two main branches of logics.

Equational theories
We discuss unification, term rewriting rules and some useful theorems related to the Church-Rosser property.
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 applications.
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.

Maintained by: Josef Schicho
Last Modification: March 1, 2000

[Up] [RISC-Linz] [University] [Search]