The Logic of Provability

General

In this course we will closely follow the book "The Logic of Provability" of George Boolos. Major themes will be Peano Arithmetic, metamathematics, incompleteness and modal logic. A provisional scheme is presented below but most likely we will not stick to it, at least not precisely. All lectures will be held in room BG 467.


Examination Forty percent of the final mark will be determined by homework assignments. Every week exercises will be handed out. The five (of six) best sessions will be taken into account. The homework is to be handed in before a new workgroup starts or before. That is, before thursday 15:00. The remaining sixty percent of the final mark is determined by an exam to be given at the end of the course. The final exam will be held thursday May 2 from 13:00-16:00 in BG 467.




Exercises Exercises come in four basic categories.
(A) indicates that this exercise is to be done for the Assesment.
(B) indicates that this exercise is included to practice some Basic knowledge which has been assumed to be known already.
(C) indicates that this exercise is among the Core material of the Course. It is almost Crucial to at least have a look at it.
(D) indicates that this exercise is a Deepening of the core material.
Combinations of categories are possible, they are to be read conjunctive. An asterisk (*) indicates extra difficulties.


Follow up This course is followed up naturally by a course of Andreas Weiermann. He will start a course on amongst others proof theory, Hilbert's programme, ordinals in proof theory, second order number theory, and Paris Harrington principles. The course will be on friday's from 11:00 - 13:00 and from 15:00 - 17:00 starting friday April 19. The lectures will be held in the mathematics department. The last lecture is foreseen to be held on June 28. The course can be taken for 7 credits but it is also possible to take it for less if one stops say halfways. The examination will be done by homework that is to be handed in (probably weekly) and possibly a final exam. In the beginning we will use the Beweistheorie notes from Buchholz. Exercises can be retrieved from Weiermann's homepage. One can look here for a route description. Also later we will continue the Lev ljectures.

Week 1 tuesday 12-03-02

Introduction. Definition of Peano Arithmetic (PA). Start on chapter 2. In the first part of this lecture we have laid out the goal of this course as can be read in the notes.
  • Notes on the first part of the first lecture
    [ Postscript| Pdf formaat]

    • After the break we started with the definition of PA. We gave a short recapitulation of first order logic in natural deduction as treated in the course Logic 2. We then treated a version of first order logic with identity as was presented in Logic and Structure of Dirk van Dalen in section 2.10. We made some general remarks on the problems and philosophical assumptions concerning identity (Leibniz 1 and Leibniz 2). For metamathematical purposes we classified natural deduction as being bad for three main reasons.
    1: proofs have a tree structure, which is hard to code.
    2: the set of proofs of tautologies is not inductively defined and the notion of open and closed assumption is opaque.
    3: it contains many rules.

    We started a Hilbert style presentation of f.o. logic as presented in Basic Proof Theory by Troelstra and Schwichtenberg. So far we have covered a part of the introduction of Boolos' book and we have started on chapter 2 elaborating on some remarks on page 18.

    Week 1 thursday 14-03-02

    Proofs in PA (ch 2).
    We have finally introduced the formal system of PA in full detail and did some formal proofs in it. Actually we only gave an almost fully detailed proof of the fact that 2+2=4. We proved theorems (2) and (7) from chapter 2. So far we have covered more or less pages 15-22 of the book.
  • Suggestions for exercises. Week1.
    [ Postscript| Pdf formaat]


    • In the workgroup we have been looking at the exercises 4-9 (referring to the new numbering!) (Remember that (A) indicates that this exercise is to be done for the Assesment.)

    Week 2 tuesday 19-03-02

    Coding of finite sequences and syntax in PA (ch 2). In this lecture we have informally sketched the technique of coding. It is indeed true that this can be done in PA as one can read in the book. We discussed Hilbert's hotel and then we gave a bijective code of pairs of natural numbers. We then switched to Shoenfield's definition that is easier but no longer bijective. Finally we multiplied by two so that we can reserve the odd numbers for other things. Some easy term was coded. We discussed the properties the formula Term(x) should posses and discussed the different levels of translation of the meta-theory in the object theory. So, objects of the part of the meta theory, i.e. formulas, are represented by numbers, while predicates about formulas (like "is provable") are represented by predicates about natural numbers. Recalling the formal definition of terms lead us to study finite sequences of natural numbers. We discussed the Chinese remainder theorem and some examples and how this theorem can be used to code finite sequences of natural numbers. These matters can be found in the book on pages 27 - 38. In the book one uses least common multiple rather than factorial. Also finite sequences are represented differently, namely as values of a Sigma-pterm. There might be a change in next week's thursday lecture.

    Week 2 thursday 21-03-02

    Modal logics introduced (ch 1). Relating different modal logics. We have introduced the modal logics K, K4, T, S4 and GL and discussed their interpretation in our programme. Also we have spoken about their epistemic interpretation. We embarked a bit on the fact that open assumptions do not exist in deductions in our normal modal logics. We also defined normality and did some deductions in normal modal logics. In the end we went back to PA and introduced the < symbol as an abbreviation. Some basic facts were proved of <. So, we covered the better part of Chapter one, and of chapter two we did some of page 22. In the work-group we paid some attention to exercises 1,4 and just a little bit on 5. Also we did 9 till 12 (d). (New numbering!)
  • Suggestions for exercises. Week2.
    [ Postscript| Pdf formaat]


    • Week 3 tuesday 26-03-02

    In this lecture we discussed the strength of PA. We introduced the class of Sigma sentences and stated completeness of PA with respect to this class. We also discussed the arithmetical hierarchy. We saw that if Goldbach's conjecture is undecidable in PA then it must be true. We also embarked on the importance of Sigma formulas by making a link with the Church Turing Thesis. The structure of the formula Bew(x) has again be considered. The Hilbert-Bernays-L\"ob derivabilityconditions have been formulated. Provable modus ponens has been proved. Also the necessitation rule. So, actually we have proved the soundness of K. Of chapter two we have so far dealt with the better part of pages 15-44.

    Week 3 thursday 28-10-02

    This lecture will be held in Amsterdam in the mathematics department to be followed up by a show in the Artis planetarium. A way to get at the maths department can be found here. The building is called "Euclides" and is on the Plantage Muidergracht 24. Later on this week the precise room will be 327 which is on the third floor. The office room of Joost is 318 and the phonenumber is 020-5256508. In this lecture we have finished the proof of Sigma completeness of PA. We have been talking about subtleties that arise when this proof is to be formalized. Without the full proof we stated that indeed the proof of Sigma completeness is formalizable. We have seen the similarity between formalizable Sigma completeness (or better a special instantiation of it) and the K4 axiom scheme. Some proofs in K4 were executed. After the break we introduced modal semantics for our logics and stated without formal proof the soundness theorems of our logics with respect to their respective class of frames. This gives us a method to show non-provability of modal logical principles.

    From the book we have dealt with pages 25,26, 15, 16 and 44-50 of chapter 2 and most of chapter 4.

    In the workgroup we concentrated on exercises 16-21 and 2-4. This week's assesment is exercise 5, 23 and 25.
  • Suggestions for exercises. Week3.
    [ Postscript| Pdf formaat]


    • Week 4 tuesday 02-04-02

    In this lecture we have repeated the mission statement that we formulated in the beginning of this course. Then we determined our position at this moment, that is, we recapitulated what we have proved so far and situated this in our programme. Then we made a start on chapter 3 defined realizations and trenslations and proved arithmetical correctness of K4 (thm 1 p 52). The diagonal lemma (corollary 2 p 54) has been proved and as an application of it we proved Goedel's first incompleteness theorem by formalizing a version of the liar paradox.

    Week 4 thursday 04-04-02

    The lecture started with the observation that in the homework one hardly uses "verbs". Use more arrows to correctly write down your argument. As an example we did some proofs in the modal logics. We also did one more example of the construction of a countermodel to show non-provability. The soundness theorems were proved for K K4 and GL by induction on proofs in the respective logics. We stated that we also have modal completeness and sketched an idea of the proof. For that purpose we defined the notions of "formula" and maximal consistent sets and reduced our goal to defining R in an appropriate way. So, we finished of the better part of chapter 4 and made a start on chapter 5.

    In the work group we have concentrated on exercises 1,3 and 13, although we did not indicate which maximal consistent sets interrelate. I further suggested (kindly) to have a look at exercises 9 and 11. Homework is 2, 9 and 10.
  • Suggestions for exercises. Week4.
    [ Postscript| Pdf formaat]


    • Week 5 tuesday 09-04-02

    In this we repeated the proof of the fixed-point theorem and applied it to prove the existence of God. A formalized version of this proof yielded Loeb's theorem and thus, by some extra work, the arithmetical soundness or correctness of GL. Later we will see that we also have arithmetical completeness which is precisely Solovay's theorem. We continued a bit on the modal completeness of our logics. We have thus dealt with the bulk of Chapter 3 (pages 51-61) and the beginning of chapter 5, (p 78- 80).

    Week 5 thursday 11-04-02

    In this lecture we have finally finished off the modal completeness theorems for K, K4 and GL. We also made a start on the arithmetical completeness theorem, that is, a start on Solovay's theorem. Thus we have finished chapter 5 of the book and made a start on chapter 9. In the workgroup we had a look at exercise 2 and discussed the exercises of the previous week.
  • Suggestions for exercises. Week5.
    [ Postscript| Pdf formaat]


    • Week 6 tuesday 16-04-02

    We discussed how the exponential function, that is, y=2^x, can be defined in PA by means of finite sequences. This method is often used. We have gone through the general structure of Solovay's proof of the arithmetical completeness. Thus we treated with the first 3 pages of chapter 9. Please read for the next session page 126 and 127.

    Week 6 thursday 18-04-02

    We finished Solovay's completeness proof for GL. Lev Beklemishev gave a view on some further topics. We spoke on Goodstein sequences and on the Hydra battle. Also we saw how ordinals are related to formal systems.
  • Suggestions for exercises. Week6.
    [ Postscript| Pdf formaat]


    • Week 7 thursday 25-04-02 13:00-15:00

    Question session. Room 467.

    Week 8 thursday 02-05-02 13:00-16:00

    Final exam. Room 467.

  • Final exam
    [ Postscript| Pdf formaat]


  • Results
    [ Postscript| Pdf formaat]






    • Vraag en antwoord


    VraagWat bedoel je in opgave twee (van week 4) met 'uniqueness of fixed points (modulo provable equivalence)'?

    Antwoord
    De dekpuntstelling zegt dat iedere formule in een variabele een zin als dekpunt heeft. Nu is de vraag of deze zin uniek is dwz ((A(B) < - > B) & (A(C) < - > C)) ====> B=C ? De vraag of de uniciteit geldt "modulo provable equivalence" is precies dezelfde behalve dat we geen gelijkheid maar equivalentie eisen indien twee zinnen beide dekpunt zijn van een en dezelfde formule. In symbolen:
    ((A(B) < - > B) & (A(C) < - > C)) ====> (B< - >C)

    Vraag
    En dan verder nog ten aanzien van het diagonaallemma: Wat is in PA |- A <-> P(A) tussen P en (A). Vervangt A de vrije variabele y in P(y) of is P een predikaat van A (bijna zoals in Bew(labda) van het voorbeeld)? Moet dus P(A) een ware uitspraak worden?

    Antwoord
    A heeft een vrije variabele minder dan P. In de gevallen die wij beschouwen is A meestal een zin en P een formule met slechts 1 vrije variabele zeg y. Met P(A) bedoelen we dan de zin (geen formule meer!) die ontstaat als de numeral van het Goedel getal van de zin A voor y in P wordt gesubstitueerd. Over de waarheid danwel bewijsbaarheid van P(A) is a priori verder niks bekend. We weten alleen dat PA |- A <-> P(A) Omdat PA een correcte theorie is weten we ook dat A <-> P(A) een ware uitspraak is.
    Joost Joosten
    Last modified: Thu May 16 14:51:26 MET DST 2002