## 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.

**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).

**References**

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