Proof Theory

Course manual 2025/2026

Course content

As objects that witness validity of arguments, proofs are a central concept in logic and, more broadly, mathematics. Formal proofs come in many styles each equipped with their own toolkit. In this course we will look at some of the standard proof systems for classical and intuitionistic logic, and discuss their main application. 

In particular, we will consider natural deduction and sequent calculus for classical and intuitionistic logics. We will prove (strong) normalisation of natural deduction for intuitionistic logic, with a detour through typed lambda calculs, and Gentzen’s Hauptsatz (cut elimination) for classical first-order logic. We will then explore key applications of the cut-elimination theorem, namely subformula property, interpolation, and consistency. As final result, we will then prove consistency of Peano Arithmetic, by devising an infinitary proof system for it, and proving cut-elimination. 

Study materials

Other

• Lecture slides/notes will be provided through the course homepage.

Objectives

• Present formal derivations in different proof calculi (Hilbert-style proof calculi, natural deduction and sequent calculus).
• Explain the main properties of these calculi (such as normalisation and cut elimination).
• Understand the difference between constructive and non-constructive reasoning.
• Recreate key concepts and techniques in proof theory.
• Demonstrate an understanding of proof theoretic methodology.
• Carry out combinatorial analyses of the structure of formal proofs.
• Critically compare different logics and proof calculi.
• Explain the role of proof theory in relation to other logical disciplines.

Teaching methods

• Lecture
• Self-study
• Seminar

Lecture course plus weekly exercise sessions.

Learning activities

Attendance

This programme does not have requirements concerning attendance (TER-B).

Assessment

• The grading is on the basis of 6 weekly homework assignments and a final exam.
• Your grade for the homework is based on the average grade you obtained on the 6 homework assignments for which you obtained the highest score.
• Your final grade is calculated as the weighted average of these grades:
  • the homework /exam ratio is 30/70;
  • an additional proviso is that the you need to score at least 50/100 points on the exam.

Inspection of assessed work

Contact the course coordinator to make an appointment for inspection.

Fraud and plagiarism

The 'Regulations governing fraud and plagiarism for UvA students' applies to this course. This will be monitored carefully. Upon suspicion of fraud or plagiarism the Examinations Board of the programme will be informed. For the 'Regulations governing fraud and plagiarism for UvA students' see: www.student.uva.nl

Course structure

Additional information

We presuppose some background knowledge in logic; roughly, what is needed is familiarity with the syntax and semantics of first-order languages. Moreover, familiarity with the notions of relations, orders and well-orders will be helpful (but not assumed). 

Contact information

Coordinator

• dr. M. Girlando