Instructor: Simone Martini
Prerequisites: An introductory course in computability. Algebra at
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.;
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
Equivalence of the natural deduction formulation with the
Notation for natural deduction proofs: typed lambda-calculus.
- 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,
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