## 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 | dorotale@amu.edu.pl |

Lecturer position | Professor |

Faculty | Faculty of Psychology and Cognitive Science |

Semester | 2021/2022 (summer) |

Duration | 30 |

ECTS | 5 |

USOS code | 23-KODL-SPT |

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