Proof theory and automated theorem proving 2021/2022 (Official code: 569076)


Lecturers: Joost J. Joosten (for the last two-and-a-half credits) and Juan Carlos Martinez Alonso (for the first two-and-a-half credits)
A course of 5 credits corresponds to around 42 contact hours. Since we do three hours a week, this will correspond to 14 weeks.
The lectures will take place in Aula 409 in the Philosophy building (Carrer Montalegre 6).

The time schedule will be Tuesdays: 10:15 -- 11:15;
Wednesdays: 10:30 -- 12:30.
The official teaching time table of the master in the first semester is given by

Docència i avaluació primer semestre

Docència: del 13 de setembre de 2021 al 4 de febrero de 2022

Avaluació continuada: del 13 de setembre de 2021 al 4 de febrer de 2022

Avaluació única: del 10 de gener de 2022 al 4 de febrer de 2022

Reavaluació: 7 de febrer de 2022 al 15 de febrer de 2022

The course consist of two parts of equal weight. The first part is on automated theorem proving and is given by prof. Juan Carlos Martinez Alonso. The second part focuses on the more theoretical part of Proof Theory and is given by Joost J. Joosten. The final grade is determined by the average of the grades obtained for the two respective parts. Homework consists of 40 % of the grade and 60 % of the grade is constituted by exams (30 % + 30 %). There will be a final exam (mid-term) in the middle of the course for the Automated Theorem proving part, and a final exam for the Proof Theory part of the course at the end. Some materials and assignments will also be placed on this page.

As mentioned, the lecturers are Joost J. Joosten and Juan Carlos Martinez Alonso. The best way to contact one of us is by sending us a mail. You can also come around to see if we're in. Joost is in the Montalegre building in Room 4045 with phone number +34 934031939. Juan Carlos has telephone number 934021661 and his office is located in the Faculty of Mathematics (Gran Via 585). Here is a link to the official course description.

We will start Wednesday, September 22. The first seven weeks will be taught by Juan Carlos Martínez Alonso and the last seven weeks by Joost J. Joosten.


Week 1 Week 2
Week 3 Week 4
Week 5 Week 6
Week 7 Week 8
Week 9 Week 10
Week 11 Week 12
Week 13 Week 14

Week 1

20/9 through 24/09. Juan Carlos starts the course on Wednesday 22.

Week 2

27/09 - 01/10

Week 3

4/10 - 8/10

Week 4

11/10 -- 15/10

Week 5

18/10 -- 22/10

Week 6

25/10 -- 29/10

Week 7

01/11 - 05/11

Week 8

8/11 -- 12/11
On Wednesday, November 10, Dr. Juan Carlos Marínez will give his last lecture.

Week 9

15/11 -- 19/11
Dr. Joost Joosten starts lecturing. In the first week we gave a philosophical and historical introduction to Proof Theory. Then we introduced the systems G3cp and G3ip from the book Basic Proof Theory (Second Edition) by A. S. Troelstra and H. Schwichtenberg. Basic terminolgy was given and we made various derivations in the system comparing them to derivations in Natural Deduction. There is some easy homework which is due before next week Tuesday 17:00.

Week 10

22/11 -- 26/11
We have shown completeness of G3cp and decidability of provability in G3cp. The homework for this week consists of Exercise 3.5.1A of the book Basic Proof Theory (Second Edition) by A. S. Troelstra and H. Schwichtenberg. You should restict your answer to the propositional fragment and the homework is due before Tuesday, December 14.

Week 10.5

29/11 -- 03/12
On Wednesday, December 1 Dr. Juan Carlos Marínez will examen the students for their midterm at the regular time and at the regular aula. On the Tuesday before that he will hold a question hour in the aula as usual at the regular time-slot.

Week 11

Since, 29/11 -- 03/12 Joosten will be at a conference and 06/12 -- 10/12 are bank holidays, Week 11 will be without classes hence. 13/12 -- 17/12

During the week, we settled doubts from the students. Furthermore, we discussed the two versions of the cut rule in G3p showing that they are equivalent provided derivability of the rules in. We gave a trivial semantical proof of cut-elimination. Next, to prepare for an informative version of cut-elimination, we prepared the stage by proving derivability of weakening, and to prepare for the derivability of contraction, we formulated and proved various versions of the inversion lemma.

Homework for this week is simple but important: Pove the inversion lemma for R/\.
All students have by way of extension till Saturday December 18 to hand the homework for last `week'. The new homework is simple, automatic but necessary to follow the course, so I will ask you to hand this in any time before class on Tuesday, December 21.

Week 12

20/12 -- 24/12
We have presented the proof of Cut elimination for G3cp. Before doing that, we had to finish the proof for admissible contraction in G3cp.

Homework for over the holidays is simple (Cut refers to context sharing):
(1) Do we have weakening for G3cp + Cut? (2) Do we have inversion for G3cp + Cut? (3) Do we have contraction for G3cp + Cut? (4) Does the proof of cut elimination for G3cp + Cut as presented in the book in Theorem 4.1.5 need in its current presentation both weakening and contraction for G3cp with Cut? And if so, is it necessary?

Have a nice Christmas and the best wishes for the new year!

Week 13

10/01 -- 14/01
We have introduced the rules for predicate logic: four of them in total. Next we saw how to change the rules to make them preserve countermodels downwards. Or formulated positively: preserve models upwards. We sketched a proof completeness of our predicate calculus. We finished by proving Cut elimination for predicate calculus. The latter proof consisted of only considering the new cases in the cut elimination proof we have seen before.

The homework for this week can be found here.

Week 14

17/01 -- 20/01
We have proven the superexponential upperbound on the length of cut-free proofs. Next we have spoken on applications of proof theory like interpolation, existence property of constructive theories and disjucntion property of various constructive theories, proof mining, consistency proofs, characterisations of provably total recursive functions, etc. The final homework of this week and of this course consists of proving d* =< d0 + d1 in Subcase 3e (for G3c) of the proof of Theorem 4.1.5.

Final Exam

Question and answer