The students should know some basic logical concepts as Naive set theory, Tarski’s semantics and at least one proof system for classical predicate logic, the completeness theorem and the compactness theorem for classical first-order logic. Knowledge of some basic algebra would be also helpful.
The goal is to enlarge the logical knowledge of the students, by presenting one of the cornerstones of mathematical logic, namely, the incompleteness theorems, and briefly introducing some more recent trends, like automated proof search
Incompleteness theorems of Goedel, Turing and Church
The notion of computable function. Church’s Thesis. Decidable sets vs semidecidable sets. Universal functions. Diagonalization. The halting set. Formal system for arithmetic. Sigma_1-completeness. Semidecidable sets are definable in arithmetic. Hilbert’s programme and the incompleteness theorems by Goedel, Church and Turing.
Automated proof search. Herbrand’s Theorem. Propositional resolution. Unification and first-order resolution.