Proof Theory

This course is part of the Mastermath programme.
Lecturers are Rosalie Iemhoff and Jaap van Oosten.
Exercise class assistant is Jeroen Goudsmit (Jeroen.Goudsmit@phil.uu.nl).

This course will be given in weeks 6-21 (February-June 2010).
The course is on Wednesdays, 10:15-13:00, in Buys Ballot Laboratory room 065, Utrecht.
The course will be concluded by a written exam. Three times during the course there will be a "bonus test" during the exercise class: a short quiz with some little problems. Doing the Bonus Tests well can earn you up to 1.5 points in the final exam. The rules are simple: your tests are graded on a scale from 0 to 1. If g is your average grade, you earn g.k.(0.5) points, where k is the number of bonus tests you took. Every Bonus Test lasts 15 minutes.

Literature: We use Chapter I and Chapter II (written by S. Buss) of the Handbook of Proof Theory. Here are some Slides for the course.

Overview of the material treated in the course

• Week 6: 1.1 A Frege proof system for propsitional logic, and a completeness theorem.
  Here are Exercises and solutions.
• Week 7: 1.2 (sequent calculus and cut elimination theorem) and 1.3.1.-1.3.4 (resolution calculus).
  Exercises.
• Week 8: 2.1 (syntax and semantics of first-order logic); 2.3 (sequent calculus and cut-free completeness theorem).
  Exercises.
• Week 9: NO LECTURE (Lecturer is abroad)
• Week 10: Start proof of the Cut-elimination theorem (theorem 2.4.2).
  Bonus Test! Here is the bonus test, with solutions. Exercise for the exercise class: do the inductive step of Lemma 2.4.2.1 for conjunction and implication.
• Week 11: remainder of 2.4.4 (cut-elimination and notion of free-cut), 2.4.5 (free-cut elimination), 2.5.1 (Herbrand theorem) and 2.5.2 (Skolemization and Herbrandization).
  Exercises on the slides.
• Week 12: 2.5.3 (General form of Herbrand theorem).
  Exercises.
• Week 13: 2.5.5 (Craig's Interpolation Theorem), introduction to Intuitionistic Logic (see slides). Exercises: see slides.
• Week 14: Carrying on with Intuitionistic Logic: Harrop formulas, negative translation. Exercises on slides and here.
  Bonus Test! Here is the Bonus Test, with solutions.
• Week 15: Start with Chapter II: arithmetic theories, Robinson's Q, various Induction, Minimization and Replacement schemes; basic number theory in I\Delta _0; defined functions and relations; Parikh's Theorem and the corollary Theorem 1.2.7.2. Exercises: prove some of the implications in the diagram on page 84 (1.2.4).
• Week 16: section 1.2 until middle of page 91. Exercises see slides.
• Week 17: rest of section 1.2. Exercises see slides.
• Week 18: Section 1.4. Quick overview of Gödel's Incompleteness Theorems. Exercises see slides.
• Week 19: Lecture by Jeroen Goudsmit: section 3.1.slides
• Week 20: Elements of Partial Recursive Function Theory (see slides); definition of intuitionistic first-order arithmetic HA, and realizability. Proof that some classically valid sentence is not realizable.
  Last Bonus Test. Here is the Bonus Test, with solutions.
• Week 21: Last lecture of the course.
• Week 24: Exam, June 15, 13:00--16:00 in Wentgebouw, room Blauw. Here is the exam, with solutions.
• Week 27: Resit, July 6, 13:00--16:00 in Wiskundegebouw, room 611ab.

Back to my teaching page