Structural Proof Theory

Timetable

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.

Syllabus

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