The aim of the course is to give an introduction to logic with emphasis on topics relevant for computer science.
The course will begin with the study of the syntax (`proof theory') and semantics (`model theory') of first order logic.
We first consider propositional logic (resolution, normal forms and Horn formulas). We then move on to predicate logic, study properties of various calculi like Hilbert systems, sequent and natural deduction calculi and prove their completeness. We derive the compactness theorem and the Loewenheim-Skolem
theorem and study some of their consequences (e.g. the existence of non-standard models).
Another important topic will be the fundamental theorem of Herbrand, its complexity and its use in unification algorithms.
Further topics are: undecidability of predicate logic, decidable fragments, Peano arithmetic and Goedel's incompleteness results.
We will also treat extensions of first order logic (e.g. second order logic), intuitionistic logic (i.e. the logic formalizing constructive reasoning) together with a discussion of the Curry-Howard isomorphism and some modal logics with their Kripke- and topological semantics. Linear logic will be briefly addressed as well. As time permits we will sketch a few other topics (e.g.
finite model theory).
A more detailed course description will be made available on my homepage.
Lecturers:
Ulrich Kohlenbach
Literature
Handouts from various books, including:
1) J. Barwise: An Introduction to First-Order Logic. In: Barwise, J. (ed.), Handbook of Mathematical Logic, pp. 5-46. North-Holland 1977.
2) U. Schöning: Logic for Computer Scientists. Birkhäuser 1989.
3) A. Nerode, R.A. Shore: Logic for applications Springer 1997.
4) D. van Dalen: Logic and Structure. Springer-Verlag 1997.
Prerequisites
Basic mathematical skills.
Course Language
English
Credits
2 points/10 ECTS credits