Proof Theory 2023/2024 (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 12 - February 2, 2024.
Re-sit period: February 5 - 9, 2023.
The lectures will take place
Wednesdays: 15:00 -- 17:00;
Fridays: 10:30 -- 11:30.
See also here.
The classes are in Calle Montalegre 6 in Aula 411 on the fourth floor.
The start date is Wednesday, September 20.
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 mainly refering to 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 18 -- 24. We discussed the general panorama of Proof Theory, arising from a long historical tradition where possibly
we can point at Aristotle and Euclid as first exponents. Modern Proof Theory
can be seen as arising from the foundational crises through Hilbert and probably only starting with Gentzen. We have mentioned some recent
developments ranging from proof assistants, to proof mining and pure proof theory.
We started the course by revisiting Natural Deduction for Minimal, Intuitionistic and Classical Propositional Logic.
The rules for Intuitionistic logic have been justified on the basis of the Brouwer Heyting Kolmogorov Interpretation.
September 25 -- 29.
We started simply typed lambda calculus and its link to natural Deduction proof through BHK.
More details are in the notes.
October 2--6.
We proved weak confluence in simply typed lambda calculus and Newman's Lemma.
EXERCISES and details are in the notes.
October 9 -- 13.
We have introduced Gentzen's G3 and seen a motivition for classical logic. That is, we have seen that
all the axioms and rules of G3 are sound. We have seen some examples of derivations in G3cp and
encourage students to make some exercises him/herself.
October 16 --20.
We have seen a sequent style formulation of Natural Deduction (Section 2.1.8).
Next, we have seen how Gentzen systems are equivalent to Natural Deducton for all three systems (c,i,m).
For this purposes we needed the Cut Rule which we added to G3.
The proof also provided a motivation of the Inversion lemmata.
October 23--27; We have proven the inversion lemma for G3cp. Likewise, we have proven the Contraction lemma.
We have spoken on the difference between admissible and derivable rules. We made a start with the proof of
the cut-elimination for G3cp. We have seen that it suffices to eliminate Context Sharing cuts.
October 30 -- November 3. There is no class on Wednesday. On Friday there is class from 10:30 -- 11:30.
We finished some of the missing cases of the proof of cut elimination.
November 6 -- November 10.
We have proven a hyperexponential upperbound for cut-free proofs. We announced that this is sharp for predicate logic (Orevkov) and
Propositional logic can do better.
We have seen a proof-sketch of Sigma(n+1) Induction proving the consistency of Sigma(n) Induction using cut-elimination.
November 20 -- November 24. We have proven an exponential upperbound for cut-free Propositional proofs. We have shown how G3cp gives rise to
a decision procedure for CPC.
There are new EXERCISES.
November 27 -- December 1. We proved cut elimination for G3ip with corresponding slightly different superexponential upperbound.
We saw a very easy version of the disjunction property. Also, we exhibited a decision procedure for G3ip and proved it terminating and correct.
December 4 -- December 8
Bank holidays, two of them.
December 11 -- December 15. We have given the proof of interpolation for constructive propositional logic.
Next we did predicate logic natural deduction with some examples and motivation. Then we did full G3 both classical and constructive.
We saw in what sense predicate logic can be reduced to propositional logic and we mentioned Herbrand's Theorem in this context.
December 18 -- December 22.
In this week we revisted our proof theoretical results and saw how they extended to the quantifier cases. In particular, we did
Lemma 3.5.2: Substitution of terms, Inversion Lemma now with all the quantifier cases included (Two are obviously not mentioned in the book);
We did the
Contraction lemmata for the quantifier cases as well as the cut-elimination for the existential cutformula.
We presented a proof of cut elimination for the universal case, proved the length invariant and the hyperexponential upperbound.
We concluded by proving interpolation for the predicate cases.
January 15 -- January 19.
FINAL EXAM: See Campus Virtual.
Question and answer
Question
The questions below refer to the final exam:
Question
In 0.3, I used G2ip + Cut (although Cut is not used) as "the corresponding (constructive) Gentzen system",
because it's the first one they prove equivalence to in Troelstra (I think).
Later, I realized you might have meant G3ip. Is it okay if I leave it with G2ip?
Answer
It is OK to use G2ip and just mention that you deviated from the one we did in class which was
indeed G3ip.
Question
I understand in 0.6 we have to give the "attempted" proof (not just the countermodel).
Answer
That's correct.
Question
In the last question of 0.6, might you have meant "fourth" instead of "second"?
I ask because the countermodel naturally read-off from the non-terminating proof of 2 seems to be already finite.
And on the contrary, 4 naturally lends itself to an infinite countermodel.
But maybe I'm misunderstanding what you meant.
Answer
The question is as I wrote: the second formula allows for a finite countermodel.
In class we discussed how you simply keep on trying to apply rules to non-provable sequents
for as long as you can to either end up with an infinite branch or with leaves that are not axioms.
Question
In 0.7, shall we give the bounds f and g for both constructive and classical logic
(as seems hinted at by the first paragraph), or only for G3cp (as seems hinted at by the last)?
Answer
You have to find the two functions for both the classical and the constructive setting and prove that the functions
that you provide are indeed good.
Question
I'm a bit confused regarding question 4: I understand we have to show (call the newly defined system G3cp') whether
G3cp' \vdash \Gamma \Rightarrow \Delta iff G3ip \vdash \Gamma \Rightarrow \bigvee \Delta.
Would this, as I assume, imply G3cp' is compatible with the BHK interpretation, or would we have to show that in a different way?
Answer
That could be an answer which is global and technical. You can also choose to go on a more lower level and
see if you can find BHK justifications for the rules. This would be a stronger and hence better argument.
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.