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.
Week 1 | | Week 5 | | Week 9 | | Week 13
Week 2 | | Week 6 | | Week 10| | Week 14
Week 3 | | Week 7 | | Week 11 | Week 15
Week 4 | | Week 8 | | Week 12

Week 1

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.

Week 2

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.

Week 3

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.

Week 4

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.

Week 5

October 13 --19. Strike and culture: no class.

Week 6

October 20--26; We have given a semantic proof of Cut-elimination. We provided arguments for a syntactical and constructive cut-elimination procedure. We have proven inversion lemmata and started with the proof of admissibility of contraction.

Week 7

October 27 -- November 2. We worked out the details of a decision procedure for propositional logic based on G3cp thereby filling in details of the semantic proof of cut elimination. For the remainder of the week we gave the syntactic proof of cut elimination. As immediate consequence of Cut elimination we mentioned the sub-formula property. We used this in a sketch of how Peano Arithmetic proves the consistency of any finitely axiomatised subtheory. Next, we started the proof on how to extract (Lyndon) interpolants from a cut-free proof of an implication. Most material came from the Blue book.

Week 8

November 3 -- November 9. On Wednesday we spent some time finishing the proof of Lyndon Interpolation. There is now homework which is due for Wednesday, November 12 before the start of the midterm exam which will take place during class hours. The homework consists of Exercise 2.5.9 of the notes. In your answer, you should at least do 3 axiom cases (one ex-falso and two identity axioms) and at least three cases of the inductive step of which at least two implication cases. We have started G3c for predicate logic dwelling on the rules, the syntax, sematics and the proof system. We have spoken about the hairy details of correct syntax and how the Blue Book deals with this through treating formulas as equivalence classes modulo alpha conversion and free-ness for substitution.

Week 9

November 10 -- November 16. On Wednesday there is a MIDTERM exam. On Friday we discussed some issues from the midterm and finished the proof of Cut elimination for predicate logic in the presentation of the Blue Book.

Week 10

November 17 -- November 23. We have discussed the results of the midterm and revisited some basic concepts thereof. Next we focussed on the increase in length that our Cut-elimination procedure can/should have. We have proven the superexponential upperbound and mentioned some lowerbound results (without proof). We have seen how to move to a single sided calculus for classical logics. To do so, we discussed the Tait language. We have seen how the semantics for the Tait language is uniquely defined by the original language. We dwelled on both first and second order examples.

Week 11

November 14 -- November 30. We have defined the operation of negation on formulas in the Tait language and introduced the calculus. Then we saw the calculus at work and proved properties like length preserving admissible weakening. We spoke of various notions of trees that are around in mathematics. Following the yellow book, our notion of tree is a particular subset of the finite consequences of natural numbers. We spoke of Bar Induction and of Bar Recursion. We have defined the order type with Bar Recursion and have seen that for each countable order type there is a tree (in our sense) whose root is of that order type. We paved the way for a completeness proof and spoke of labeled trees.

Week 12

December 1 -- December 7

Week 13

December 8 -- December 14.

Week 14

December 15 -- December 20.



FINAL EXAM: See Campus Virtual.

Resit

Question and answer

Question

I wanted to ask you about the homework exercise that we have to do for wednesday. I am confused as to what exactly we have to do. To me it seems we have to redo the same proof (by induction on the proof), but now doing aaaalllll the cases and just check how much it grows the proof at each case, then we take the worst case scenario and that's it. I don't know if that is what you want us to do. Thanks on advance!

Answer

More or less this is what you have to do. However, (worst-case) growth at each step will have to be reflected in the final growth of the interpolation formula. Remember that eliminating one single cut leads to roughly doubling the proof length but eliminating all cuts leads to hyper-exponential growth rate. So your observations per step need to be collected into an overall growth-rate that can be taken along in your induction. Also, I mentioned that not all cases are needed and mentioned a minimal amount. Also, I have feeling that this exercise may be good for the midterm exam.

Question

I assume that the "take the worst case to see what's the bound" part of my question was correct since there is no answer to that.

Answer

Sort of. In a sense you are asked to bound the worst-case scenario with a slowest possible growing function. You can bound linear growth by a hyperexponential function but that will not be too informative... It is allowed to work in groups on this exercise. Just acknowledge with whom you have collaborated and hand in your own answerset. It could also be an idea that some students hand in some cases and the other cases are handed in by other students. The idea is that you learn from this and that you enjoy working on it. As a side effect you may memorise some of the rules :-)

Question

I am stressing over how overwhelmed I find myself by the midterm.

Answer

Don’t worry. I gave some very juicy hints. Just follow them and all will be fine. Don't forget to also practice some derivations in Natural deduction and revisit the exercise on the Curry Howard Isomorphism and the Brouwer Heyting Kolmogorov Interpretation. I advice you to organise some sessions with various students together to help each other out.

Question

In order to formalize induction, I suppose we need predicate logic, not just propositional logic. Here is how I am reasoning:

Here is how I am reasoning:

To show PA ⊢ Con(Σ) for any finite subset Σ of PA, it seems enough to show that IΣn+1 ¬⊢ IΣn ⇒ 0=1.

Assuming it does, there would then exist a cut-free proof of IΣn ⇒ 0=1 (in which system, exactly?).

My question is the following: we have seen the cut-elimination theorem for G3 (say, also for the predicate case), so I am not sure what the cut-elimination theorem would look like for our system IΣn+1.

My guess is that we obtain a cut-free proof of IΣn ⇒ 0=1 in G3 (for predicate logic) with the language of PA, and then we use the fact that it is cut-free to conclude IΣn+1 ⊢ IΣn ⇒ 0=1.

Once we have this, since N ⊨ IΣn+1, it would also satisfy the sequent IΣn ⇒ 0=1.

Am I correct in saying that this means N satisfies the interpretation of that sequent? If so, the contradiction would follow, I think.

Thanks in advance on behalf of myself and my colleagues,

Answer

You are right that we need Cut elimination for predicate logic. We can use this as a black box. As to your reasoning: Let us hope that IΣn does not derive a contradiction :-) Remember when some system of arithmetic T proves the consistency of some system S, then really we should code the statement of consistency into the language of T, arithmetic in this case. Through Gödel coding we know how to do this. So in our case T would be PA (Peano Arithmetic). Suppose S is a finite fragment of the axioms of PA. Now, reasoning in PA, suppose that S proves 0-1. Then, by the Deduction Theorem we would under this assumption be able to prove in pure predicate logic that the conjunction of the axioms of S imply 0=1. Apply cut-elimination to this proof so we get a proof with the subformula property. Since S is finite, there is a maximal quantifier complexity of S. Now use a partial truth-predicate for this complexity class and prove by induction on the length of the proof that All of the Antecents prove some of the Succedent. Since PA proves all of S (S was a subsystem) we would get inside PA that 0=1 and PA can prove that this is false so we get a contradiction.

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.