The Logic of Provability and Interpretability

This course consists of two parts. The first part will dwell on the logic of provability and is quite similar to the course I taught previous year. The second part will deal with the logic of interpretability and is new.

This course will be held in the fourth period of the academic year 2002-2003. The course will be held at the Uithof which is not so difficult to reach. The philosophy department is located at the Bestuursgebouw and all the lectures will be held in room 467. The first lecture is on wednesday April 23 at 11:00. For the moment the lectures are scheduled on mondays 11:00-13:00 and wednesdays 11:00-15:00 but this might very well change from week to week. (In the official schedule this course is referred to by CS toegepaste Logica A wb3054.) Please consult this page for the latest updates. Also, by sending me an email you can submit to a mailinglist to get informed.

In each lecture I will try to let one student do a little presentation. These are really to be thought of as minute presentations of say maximally ten minutes in which for example a theorem from the course-book is proved. The presentations add up to the final result in a way that is described below. One of our three weekly sessions will be a working group. Every week, exercises are to be handed in. These exercises will for a significannt part make up the final mark. Halfway there will be an exam which together with the final exam and the previously mentioned part make up the final mark.

Examination The final mark will be assigned in the following way. 15 percent of the final mark is determind by the exam that comes halfway. 35 percent is determined by the home-work and the reaming 50 percent comes on account of the final exam. The presentations will provide an additional bonus. Presentations will be marked in a binary way, so to say. That is, either you do the presentation and you get the full score or you don't and obtain a zero. Later I will fill in how precisely will the bonus be taken into account. The course is given during ten weeks. The eight (out of ten) best sessions of homework will be used to make up the final mark for the homework part. All marks are on a scale from 0 to 10. If h denotes the homework, e the exam in between, E the final exam and b the bonus. The final mark F will be calculated by the following formula:
F= Min ( 10, 0.15 * e + 0.35 * h + 0.5*E + b ).

Week 1 wednesday 23-04-03 11:00-13:00

A general introduction to the subject and an exposition of our scheme. Philosophical repercussions. Lucas' argument. We also discussed the importance of the set-theoretical environment, like the existence of large cardinals, in which one works. There was a handout covering a part of the introduction. For philosophical reading we suggested Logic, Logic and Logic from Boolos. There is also some notes written by me which were discussed in class.
  • [ Postscript| Pdf formaat]

    • Week 1 wednesday 23-04-03 13:00-15:00

    The object theory PA (Peano Arithmetic). Getting acquainted. We started on Chapter two of the book The Logic of Provabiliry of Boolos. We have treated the language of PA, we have given a definition of terms using the notion of a sequence building it up. We have done the same for formulas. We have given the axioms and proved A->A in a Hilbert style calculus. So far, we have treated of Chapter 19 up to and including page 19.

  • Exercises Week 1
    [ Postscript| Pdf formaat]

    • The homework exercises for this week are 1, 2, 5 and 11. They are to be handed in before wednesday next week.

    Week 2 Monday April 28, 11:00-13:00

    Nick will repeat the proof of A -> A in the Hilbert calculus. Tom will prove Theorem 2 on Page 21. More on the object theory. We will prove Sigma completeness of PA. The notion of truth we refer to is just the truth in the standard model of the natural numbers. Of course this may depend on the set-theoretical environment one works in but as we shall see in due course we do not need that much of the set-theoretical universe for the time being. For those who want to be completely precise we can say that we work in the standard model of the natural numbers as this is embedded in ZFC. Here I give a link to a note by Kees Doets on the axioms of ZFC.

  • An Introduction to Zermelo Fraenkel, A selection of notes of Kees Doets(modified)
    [ DVI | Postscript]

    • Week 2 Friday May 2 13:00-17:00

    We introduced the arithmetical hierarchy and proved Sigma_1 completeness. We already hinted at the proof in a formalized setting.



    For a nice and readable introduction to our studies, see also Verbrugge's overview.

    Week 3, Wednesday May 7. 13:00-15:00, BG 467

    Marieke will prove Lemma 21 on Page 27. Coding pairs and coding finite sequences. Representing the meta-theory in the object theory. Coding proofs. Properties of the provability predicate.

  • Exercises Week 2
    [ Postscript| Pdf formaat]

    • The homework exercises for this week are 7, 8, 20, 21 and 22. They are to be handed in before friday of this week.

    Week 3, Friday May 9. 13:00-17:00, BG 465

    Modal logic (and its provability interpretation). We looked at the coding of finite sequences of numbers into one number. The engine behind this was the Chinese remainder theorem. We also studied the coding of pairs of natural numbers into one natural number. We looked at natural predicates stating that x is the code of a term, of a formula and of a proof. Finally we could formulate the predicate Bew(x). We have shown two very important properties, namely those that translate in the modal language to distributivity and necessitation.

    After the break we introduced the modal logics K, K4 and GL and worked a bit with them. So far we have covered more or less from the book: Chapter 2 (p.15-p.46), Chapter 1 (p.1-p.7). In the working group we looked at the exercises 42-45(a)and (b), 7,8,12 and 13.

  • Exercises Week 3
    [ Postscript| Pdf formaat]

    • This week's homework is exercise 14, 29, 30, 31 and 45 c-i to be handed in before thursday May 15.

    Week 4 Monday May 12 11:00-13:00, BG 467

    We did some more derivations in the modal logics K, K4 and GL. Basicly we finished Chapter one. We then turned to modal semantics and dealt with the first four pages of Chapter 4. For an introduction to the subject of modal logic, see: a paper by Robert Goldfarb.

    Week 4 Thursday May 15 9:00-11:00

    Modal completeness. Chunlai will give a presentation of Theorem 24 (a) of Chapter 1. We will deal with Chapter 4 and 5. We have treated the frame conditions of both K4 and GL. Also have we seen some applications of modal semantics to non-provabilty results. Nick tipped me for the following link on Boolos.

    Week 4 Thursday May 15 14:00-16:00

    Work group.

  • Exercises Week 4
    [ Postscript| Pdf formaat]

    • The homework of week four consists of exercises 20 and 23 a,b and c.

    Week 5 Monday May 26 Room 467; 11:00-13:00

    Modal completeness. PA again. Arithmetical soundness of K. Labeled frames. Lindenbaum's lemma. We are almost done with the modal completeness of GL. That is to say, we outlined the step-by step method and will fill in the details next wednesday. We have discussed the contents of Chapter 4 from Boolos (only the ones concerning K, K4 and GL).
  • Handout on the step-by-step method
    [ Postscript| Pdf formaat]

    • Week 5 Wednesday 28 Room 467; 13:00-17:00

    Soundness of Gl. We have discussed the step-by-step method. Proved modal completeness for GL and found countermodels applying the step-by-step method. Another method (a rather similar one) can be read in Chapter 5 of Boolos.

  • Exercises Week 5
    [ Postscript| Pdf formaat]

    • The homework for Week 5 consists of exercises 1,7, 9 and 14. (quite some work!)

    Week 6 Monday June 2 Room 467; 13:00-15:00

    Provably Sigma_1 completeness. We have discussed the properties of substitution and started a proof of provable Sigma_1 completeness. The rest of the proof is to be read by the students. Thus we have finished Chapter 2 completely.

    Week 6

    Soundness of K4. Diagonalization lemma. Arithmetical soundness of GL. Arithmetical completeness of GL: what is Solovay's theorem? We have thus covered the first part of Chapter 3 (say up to and including Theorem 2).

  • Exercises Week 6
    [ Postscript| Pdf formaat]

    • The homework for Week 6 consists of exercises 1 and 2, that is, all the exercises of Week 6.

    Week 7 Tuesday June 10 13:00-15:00

    Arithmetical completeness, Solovay's theorem. We have treated the first half of Chapter 9. (Say, up to and including Lemma 1.)

    Week 7 Wednesday 11 14:00-17:00

    Mid term exam.

  • Midterm exam
    [ Postscript| Pdf formaat]

    • Week 8 Monday 16, 13:00 - 15:00, room 467

    Interpretability and formalized interpretability. The logics IL and ILM. Starting on the modal semantics for IL and for ILM. Arithmetical soundness of some principles of ILM. We gave an introduction to the topic of interpretability. Most of the material is covered by the first two sections of a paper called Formalized Interpretability in Primitive Recursive Arithmetic, ps-format, pdf-format.

    Week 8 Wednesday 18, 13:00-17:00

    Modal semantics. Start with the modal completeness. Some of the material treated can be found in the notes of lecture 16 [Postscript| Pdf formaat].

    The homework for this week is exercise 2.10, 2.11, 3.4 and 3.7.8.

    A treatment of the semantics can be found in many places. For example Visser's overview paper on interpretability. But also my Masters thesis is sufficient.

    Week 9 Monday June 23 13:00-17:00, first in BG 467, later (if necessary) Trans 1. 115

    Modal completeness and the step-by-step method. We have proved the main lemmata and discussed the complexity of the proces. Some aspects were treated. A fully detailed treatment can be found in the masters thesis. An article is to appear soon. See some notes in my masters thesis on this, ps-format, pdf-format.

    Week 9, Wednesday 25 in Amsterdam: Optional

    ********************************************************
    * *
    * *
    * THE LOGIC TEA *
    * *
    * *
    ********************************************************

    Speaker: JOOST JOOSTEN, Utrecht University
    Title: USING INTERPRETATIONS IN COMPARING THEORIES
    Place: Euclides Building, room P.014
    Plantage Muidergracht 24, Amsterdam
    Time: Wednesday, June 25
    3-5pm (sharp)

    You are most cordially invited! Tea and cookies will be
    served.

    For more information, please contact Boudewijn de Bruin
    (debruin@science.uva.nl) or Mark Theunissen (mtheunis@science.uva.nl),
    or check the web site at
    http://staff.science.uva.nl/~debruin/logic_tea.html.


    Abstract
    This talk will introduce a broad audience to the ways in
    which interpretations may be used to compare the strengths
    of theories.


    Week 9 Thursday June 26, 14:00-16:00, BG 467

    Gödel's completeness theorem. Formalizing Gödel's completeness theorem. Orey-Hájek characterizations. Of the Orey Hájek characterizations we only dealt with the Pi-1 conservativity (in case of sufficient induction). Arithmetical soundness ILM. So, the soundness of the J5 axiom could be seen by formalizing Gödel's completeness theorem. The M axiom follows from Π-1 conservativity (which we did not prove). There are no notes on the formalized completeness theorem but this part of the theory will not be needed in full detail in the exam. A sufficient treatment can be found in Visser's paper "Formalizing Interpretability" or De Jongh and Djaparidze's contribution to the handbook of proof theory "Provability Logic".

    Week 10 13:00-16:00, BG 467

    Final exam
  • Final exam
    [ Postscript| Pdf formaat]

    • Joost Joosten
    Last modified: Tue Oct 7 14:31:41 MET DST 2003