Proof Theory 2025/2026 (official course code 575366)
Organisation
Here an academic year calendar of the UB can be found.
For us it is important to know:
Teaching period (including exam): September 15 - January 30, 2026.
Re-sit period: February 2 - 6, 2023.
The lectures will take place
Wednesdays: 15:00 -- 16:30;
Fridays: 10:30 -- 12:00.
The classes are in Calle Montalegre 6 in Aula 402 on the fourth floor.
The start date is Wednesday, September 17.
TO BE UPDATED
The page below will be updated as we proceed.
The final grade is determined by
(A) Homework questions (this may include a mid-term exam); (20 %)
(B) Presentation in class (0 %);
(C) Midterm + Final Exam; (30 + 50 %).
All materials and assignments will also be placed on this page.
Joost J. Joosten is the lecturer of this course.
We will be starting with the book Basic Proof Theory
by
A. S. Troelstra & H. Schwichtenberg (Second edition).
The Proof Theory course constitutes for 5 European credits and as such comprises 42 contact hours, so that makes 14 weeks, 3 hours each.
September 15 -- 21.
We gave a historical and philosophical introduction to Proof theory. Next we started out with parts of Chapter 1 of the book
Basic Proof Theory (Second Edition) by Troelstra and Schwichtenberg. In particular we have seen natural deduction for the
implicational fragment of minimal logic. We discussed the BHK interpretation and saw a rudimentary version of the Curry-Howard Isomorphism
(terms as proofs) for simply typed lambda calculus where beta-reduction corresponds to a conceptually clear proof transformation.
September 22 -- 28.
Wednesday was a bank holiday. On Friday we spoke of lambda calculi both typed and untyped.
We have seen etha reduction and its pendant under the Curry-Howard Isomorphism.
We introduced the combinators S and K in the untyped setting.
We have seen that lambda abstraction can be mimicked in the setting of Combinatory logic.
A good reference for reading about this is the book "The lambda Calculus, its Syntax and Semantics" by Henk P. Barendregt.
Also the blue book has some background in Chapter 1.
Ther is a first batch of exercises which is due for Monday, October 5.
September 29--October 5.
On Wednesday we have given the definition of various systems of Natural Deduction.
We have seen how certain proofs lack the subformula property. For example, a proof of Peirce's formula.
October 6 -- 12.
We have introduced the system G3_cp as in the Blue book. We have proven soundness and seen some derivations.
We have spoken about some motivations and about the reversability of the rules.
We have discussed some of the homework. We have proven the admissibility of weakening in G3_cp.
October 13 --19.
October 20--26;
October 27 -- November 2.
November 3 -- November 9.
November 10 -- November 16.
November 17 -- November 23.
November 14 -- November 30.
December 1 -- December 7
December 8 -- December 14.
December 15 -- December 20.
FINAL EXAM: See Campus Virtual.
Question and answer
Question
Question
Answer
Question
Answer
Question
Answer
Question
Answer
Question
Answer
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.