Written exam

Course instructor: PhD Melissa Antonelli

Content:
This course offers a gentle introduction to (structural) proof theory, focusing specifically on sequent calculi for propositional logic. Students will explore the historical and technical significance of these systems while developing the skills to construct formal derivations and prove key meta-logical results. Time permitting, we will extend these methods to modal propositional systems. This is an active learning course; sessions involve a mix of lectures, collaborative exercise solving, and peer feedback to ensure a deep, practical understanding of the material.

Completion requirements:
Attendance of seminar classes, active participation in exercise sessions and the forum, and a final exam. Attendance is mandatory, though motivated absences are accepted.

After completing the course, participants will:

- Understand the relevance of (structural) proof theory and become familiar with sequent calculi for several propositional logic systems;

- Distinguish between classical and intuitionistic propositional logic;

- Apply inferential rules and construct formal derivations;

- Master standard techniques to establish logical properties and prove basic meta-theoretic results (e.g., invertibility of rules, cut-elimination, soundness and completeness);

- Evaluate and provide feedback on the correctness of derivations and proofs.

Literature:
S. Negri & J. von Plato, Structural Proof Theory, Cambridge University Press, Ch. 1-3;
S. Negri & J. von Plato, Proof Analysis, Cambridge University Press, Ch. 11.

---

Prerequisites:
The course is designed to be self-contained. There are no formal prerequisites, though a first course in logic is recommended.