Mathematical Logic

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.

Program

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 II and III:
* D. vanDalen, Logic and Structure, Springer-Verlag
* J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press