Proof theory and automated theorem proving (Official code: 569076)
Organisation
Lecturers: Joost J. Joosten (for the first 3 credits) and Juan Carlos Martinez Alonso (for the last two credits)
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).
The first eight weeks will be taught by Joost.
Wednesday 13-02-2013
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.
Friday 15-02-2013
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.
Wednesday 20-02-2013
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.
Friday 23-02-2013
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.
Here is an example of a derivation in Tait-calculus.
Wednesday 27-02-2013
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.
Friday 01-03-2013
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 ω1CK. In class we had a slightly different definition of this ordinal than in the book but by using something similar to "Craig's trick" we can see that both definition are actually equivalent. From now on we shall stick to the definition as given in the book. Next we spoke on the definition of a search tree and you are kindly asked (required :-) ) to read the definition of this search tree which is on pages 57 and 58 of the book before next Wednesday. This assignment together with the exercises which are the exercises are due for next Wednesday is probably quite some work. This week, apart from Exercise 1.1, the exercises are more difficult than before.
Here are the answers to this set of exercises as provided by Cory.
Wednesday 06-03-2013
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).
Friday 08-03-2013
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.
Wednesday 13-03-2013
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.
Friday 15-03-2013
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.
Wednesday 20-03-2013
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.
Friday 22-03-2013
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.
Wednesday 03-04-2013
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.
Friday 05-04-2013
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.
Wednesday 10-04-2013
Friday 12-04-2013
15 -- 19 Abril, Midterm exam
From here on Juan Carlos will be teaching. IMPORTANT, THERE IS A CHANGE IN THE TIMETABLE. In all dates below, the Wednesday date should be replaced by the Tuesday before (now bank-holidays differ! For example Tuesday 23 is free due to Sant Jordi, but April 30 is no longer a bank holiday where May 1 was, etc.). So, instead of the Wednesday, Juan Carlos will teach on the day preceding it. More precisely, Juan Carlos will be teaching Tuesdays in room 406 (Montalegre building) from 15:30 -- 17:00.
Wednesday 24-04-2013
Friday 26-04-2013
Wednesday Labour day, no classes
Friday 3-05-2013
Wednesday 8-05-2013
Friday 10-05-2013
Wednesday 15-05-2013
Friday 17-05-2013
Wednesday 22-05-2013
Friday 24-05-2013
Wednesday 28-05-2013
Friday 31-05-2013
Wednesday 19-06-2013
Aula 412 (regular class-room at the Montalegre 6 building);
Time: 16:00-19:00
Question and answer
Question
Q: (About the exercises of Week 3)
Can you give me a hint about how to embark the p.r. for w^w???
Answer
A.: You could try sequences of arbitrary (finite) length here and order them as in a dictionary.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.