Introduction to logic

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.