A course of 5 credits corresponds to 40 hours of contact hours.

The lectures will take place in Room 412 at the philosophy department at Montalegre.

Wednesdays: 18:00 -- 19:30;

Fridays: 9:00 -- 10:30.

The final grade is determined by

(A) Weekly homework questions; (35 %)

(B) Midterm take-home exam; (25 %)

(C) Final Exam; (40 %).

All materials and assignments will also be placed on this page. We shall mainly work from the book Proof Theory by Pohlers (subtitle: The First Step into Impredicativity) published at Springer, 2009.

The lecturers are Joost J. Joosten and Juan Carlos Martinez Alonso. Joost will teach for the first eight weeks and Juan Carlos for the remaining weeks. 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).

Week 1 | Week 2 | |

Week 3 | Week 4 | |

Week 5 | Week 6 | |

Week 7 | Week 8 |

We have given an very brief general and historical introduction to proof theory and spoke on how the course is organized. Next we defined proofs in Natural Deduction for proofs that using introduction and elimination rules for conjunction, and implication. Moreover, we have discussed the falsum rule. Note, we work in a propositional language where the $\neg A$ is an "abbreviation" of $A \to \bot$. (Yes, that's Latex.)

The homework, due next Friday, consists of sending me an email and making five natural deduction derivations. You can find the questions here.

We have spoken about the Brouwer-Heyting-Kolmogorov interpretation of Intuitionistic propositional logic, and completed the ND deduction system with the three disjunction rules and with the RAA rule. We spoke about completeness and soundness of both classical and intuitionistic propositional logic and of their complexities (CoNP vs PSPACE).

Here are the exercises which are due for next Wednesday. You should hand in answers to question to Items 12, 16, 18, 19 and 20 from the first question. Items 1 and 6 from the second question, and Items 2 and 3 from the Third question.

Here are the answers to the first set of exercises as provided by Cory. This is a zipped directory that apart from the answers, contains a tex-file with the solutions. Those of you who have little experience in Latex might use this to make their future exercises. Just read on the internet how to install Latex, and where to store style-files etc. For any questions, ask one of your fellow students, or Joost. Here are the answers to the first set of exercises as provided by Cory.

We have spoken on how each inductive definition comes with a corresponding proof principle. Next we discussed what valid reasoning involving quantifiers should look like an how this is reflected in our Natural Deduction systems (classical and intuitionistic). We saw some constructive proofs in ND using the rules for the quantifiers. Here are the exercises which are due for next Friday. You should make all of Exercise 1, but only Item 4 of Exercise 2.

Here are the answers to this set of exercises as provided by Cory.

We spoke about three major drawbacks in ND proofs. Then we spoke in general on sequent calculi and finally we dealt with one-sided Tait Calculus in the Tait language. From now on we work from the book of Pohlers so I can refer to the parts that were covered in class. So till now we have dealt with Chapter 4 of the book up to Definition 4.3.2 (including it). Please read this over again as I will assume you know it at the next class. Here are the exercises which are due for next Wednesday. You need only hand in Exercises 4 and 5. Note, that in Ex. 5 you will first need to apply a translation. Moreover, you are strongly encouraged to make some derivation in the Tait calculus in propositional logic. Here are the answers to this set of exercises as provided by Cory.

We have proven soundness of the Tait-calculus. Next we started to outline the strategy to prove completeness using Schütte's method of search trees. PLease, read Sections 4.2 and 4.3 of the book (Section 4.1 provides certain motivation but is maybe better read afterwards). Further, we spoke on the formalization of trees (Definition 4.4.2). Next Friday we shall shortly revisit the notion of Primitive Recursive Function (Chapter 2) and some basics of ordinals (Chapter 3, Sections 1 and part of 2) so that we prepare for completeness proof of our Tait calculus (Section 4.4).

The homework, due for next Friday consists of the simple exercise 4.2.11 of the book.

Today we have revisited primitive recursive functions and as such looked at Chapter 2 of the book. In particular we looked at a way of coding finite sequences of natural numbers as natural numbers and convinced ourselves that this is indeed primitive recursive. We spoke a bit on ordinals and in particular gave the definition of ω

We gave the definition of our search trees and started on the proof of the Syntactical Main Lemma. The homework due for Friday is: Provide the searchtree for M = A \/ B and Delta = A \/ B (that is, both M and Delta consist of the same formula (singleton) with A and B atomic).

We have presented the proofs of both the syntactical and the semantical main lemmata thereby finishing the completeness proof of the Tait calculus for f.o. predicate logic. Here are the exercises which are the exercises are due for next Wednesday. This week the exercises are rather easy and you are only asked to hand in Exercise 2.

We proved that the cut-rule is admissible for the one side Tait calculus for first order logic, thereby providing a non-constructive cut-elimination proof. Further, we started on Chapter 5 of the book introducing an infinitary verification calculus for first order logic. We have proven that this calculus is sound and complete using only finite ordinals for first order logic. On Friday we shall see that for Pi^1_1 sentences (we introduced the arithmetic and analytic hierarchy too) the infinitary calculus needs larger ordinals. There is NO homework for next Friday.

Of Chapter 5, we have Finished up to and including Section 5.3. Here are the exercises which are the exercises are due for next Wednesday.

We have finished all of Chapter 5. In particular, we have proven the Omega Completeness Theorem. Since this nicely closes off one theme there will again be NO exercises for next Friday.

Inductive definitions: we have introduced the definitions of the proof-theoretic ordinal of a theory and the Pi^1_1 ordinal of a theory as given at the beginning of Section 6.7 of the book. Next we discussed all material in Sections 6.1--6.3. Here are the exercises which are due for Wednesday April 3.

We have briefly recalled the basic notions of Chapter 6 and then dealt with the remaining Lemma 6.3.4 from Section 6.3. Next we dealt with Sections 6.4 and 6.5. Homework, due for next Friday is: Prove that for any binary relation < on the naturals, when restricted to Acc_<, this relation < defines a well-founded relation.

On Friday, we have dealt with part of Section 6.6. In particular, we have proven Lemma 6.6.2 and we have done all of Page 95 up to and including Corollary 6.6.11. However, we have skipped quite some details and part of the homework is to read over the details. Also we have revisited the definitions on Page 100 and hinted at Theorem 6.7.3. The homework due for next Wednesday is included here and consists of Exercise 2.

Friday 12-04-2013

Wednesday 24-04-2013

Friday 26-04-2013

Friday 3-05-2013

Friday 10-05-2013

Friday 17-05-2013

Friday 24-05-2013

Friday 31-05-2013

Aula 412 (regular class-room at the Montalegre 6 building);

Time: 16:00-19:00