Mathematical Logic

Instructor: Simone Martini

Prerequisites: An introductory course in computability. Algebra at junior level.

Aims: The first part of this mathematically oriented course will provide a deep introduction to the main concepts and results of logic which are at the basis of most theoretical computer science. The other parts will focus on fundamentals of proof- theory and their relations to typed lambda-calculus and, thus, functional programming.


Part I: Fundamentals (~50%)
Formal systems for first order logic: syntax and semantics (`a la Tarsky).
Soundness and completeness theorems; compactness th.; Loeweinheim-Skolem th..
Undecidability of first order logic (sketch).
Peano arithmetic; non-standard models.
Goedel's incompleteness theorems.
Part II: Fundamentals of proof theory (~30%)
Natural deduction systems for first order logic. The constructive interpretation of logic: intuitionistic logic. Equivalence of the natural deduction formulation with the axiomatic formulation. Notation for natural deduction proofs: typed lambda-calculus. Normalization, confluence. Semantics.
Part III: Linear Logic (~20%)
Multiplicative linear logic: sequent formulation; proof-nets; phase semantics. Relations with concurrent systems (Petri nets).
Part I: any good logic textbook, like
* Bell and Machover, A Course in Mathematical Logic, North-Holland.

Part II and III:
* D. vanDalen, Logic and Structure, Springer-Verlag
* J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press