Logic II for Mathematicians and Computer Scientists
Tuesday, 13:00 - 14:30, KHG 2.
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.
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
- 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).
- We discuss lambda calculus with respect to
two main applications: as a foundation for functional programming,
and as a language for higher order logic.
- Constructive Logic
- We give Goedels's negative translation of
intuitionistic logics into classical logics.
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.
B. Chang and C. Lee.
Symbolic Logic and Mechanical Theorem Proving.
Academic Press, 1973.
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,
Stetigkeit und irrationale Zahlen.
H. Ebbinghaus, J. Flum, and W. Thomas.
H. Schwabhäuser and W. Szmielev and A. Tarski.
Metamathematische Methoden in der Geometrie.
Grundlagen der Geometrie.
D. Hilbert and P. Bernays.
Grundlagen der Mathematik I und II.
Automatic theorem proving 1 and 2.
Lectures at the university of Linz, winter 1998/99 and summer 1999.
A. Jones and Y. Matijasevic.
Proof of the recursive unsolvability of hilbert's 10th problem.
Am. Math. Monthly, 98:689-709, 1991.
Introduction to Metamathematics.
A course in mathematical logic.
First Order Mathematical Logic.
J. Pfalzgraf and D. Wang.
Automated practical reasoning.
On the computational complexity and geometry of the first-order
theory of the reals.
Journal of Symbolic Computation, 13(3):255-300, 1992.
First order logic.
A Decision Method for Elementary Algebra and Geometry.
Univ. of California Press, Berkeley, second edition, 1951.
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.
A. Troelstra and D. van Dalen.
Constructivism in Mathematics.
Maintained by: Josef Schicho
Last Modification: March 6, 2001