General information

Course type AMUPIE
Module title Structural Proof Theory
Language English
Module lecturer prof. UAM dr hab. Dorota Leszczyńska-Jasion
Lecturer's email
Lecturer position Professor
Faculty Faculty of Psychology and Cognitive Science
Semester 2021/2022 (summer)
Duration 30


Module aim (aims)

The aim of the course is to acknowledge the listener with the main tools of structural proof theory. The course is a concise introduction to structural proof theory: its origins, its main tools, and the consequences of the famous admissibility results (cut elimination). The focus is on sequent calculi for classical, intuitionistic, and minimal logic; however, natural deduction basics are also introduced. An emphasis is placed also on the techniques of proving cut elimination.

Pre-requisites in terms of knowledge, skills and social competences (where relevant)

Basic knowledge of classical logic: both propositional and first-order.


Week 1: The origins of structural proof theory
Week 2, 3: Gentzen’s natural deduction system for intuitionistic and classical logic
Week 4: Jaśkowski’s natural deduction system
Week 5, 6: Gentzen’s sequent calculus for intuitionistic and classical logic
Week 7, 8: Secondary and admissible rules, admissibility and eliminabiity
Week 9, 10: Strategies of proofs of eliminability of structural rules
Week 11, 12: Consequences of cut elimination
Week 13-15: Applications of structural proof theory in metamathematics

Reading list

Negri, S. and von Plato, J. (2008) Structural Proof Theory, Cambridge University Press
Negri, S. and von Plato, J. (2011) Proof Analysis, Cambridge University Press
Troelstra, A.S. and Schwichtenberg, H. (2000) Basic Proof Theory, Cambridge University Press