1. Course notes (downloadable from Moodle).
2. A.S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge University Press 1996.
3. S. Negri, J. von Plato, Structural proof theory, Cambridge University Press 2001.
4. J.R. Hindley, J. Seldin, Lambda-Calculus and Combinators, an Introduction, Cambridge University Press 2008.
(i) Knowledge and understanding. Knowledge of the main theoretical issues and methodologies in structural proof theory, combinatory logic, (typed/untyped) lambda calculus. Understanding specific problems in these areas.
(ii) Applying knowledge and understanding. Applying the above knowledge and understanding though suggested exercises dealing with specific problems in the areas of logic and philosophy of logic.
(iii) Making judgements.
Critical understanding of scientific contributions (articles, books) in an autonomous way.
(iv) Communication skills.
Ability to present in an appropriate way problems, solutions to problems, theories, arguments, proofs.
Background knowledge corresponding to the program of the Logic 1 course (12 CFU)/ BA level. Contact the teacher before enrolling in the course.
Lectures, plus tutorial
Course materials (lectures notes, exercises etc.) will be available online at the Moodle page of the course.
The course requires a regular attendance (at least 2/3 of the lectures).
Type of Assessment
Oral examination (about 45 min.), typically based on two questions for each of the two parts of the program (proof theory; theories of operations). The student should be able to explain in a clear and appropriate language the main theoretical notions taught during the course, as well as to apply them correctly to the solution of simple exercises/problems.
(i) Introduction. Propositional and predicate classical logic: syntax and semantics (recap);
(ii) sequent calculi (Gentzen's L-calculi; G3-style calculi) for first-order classical and intuitionistic logics;
(iii) cut-elimination and its main applications (including Maehara's lemma and interpolation theorem; Herbrand's theorem);
(iv) (hints to) substructural logics, in particular affine linear logic and linear logic;
(v) combinatory logic and untyped lambda-calculus; Church-Rosser theorem with applications; fixed-point theorem and applications;
(vi) typed lambda-calculus; normalization and Curry-Howard correspondence.