Here is the draft final chapter of Part I of Beginning Mathematical Logic — so this is the last of the group of chapters on core topics at an elementary level. This one on proof theory is newly written; comments will therefore be particularly welcome.
Having got this far, I am well aware that there are now some mismatches in the level/breadth of the overviews in the various chapters, and also places which call for more cross-references. For example, I need to go back to the overview on set theory to say just a paragraph or so more about ordinals, in order to make a better connection with the use of small ordinals in the current chapter when waving my arms at Gentzen’s consistency proof. So smoothing out the coverage of Part I of the Study Guide is a next task. But at least there is now a full draft to play with.
I’ve been reading and very much enjoying the drafts of the new study guide. I especially enjoyed this one on proof theory: very clear and engaging. I meant to post these typos and a comment weeks ago but other things have got in the way. Anyway, here they are. First the comment/suggestion:
p. 103 “we have found how far along the ordinals we need to run our transfinite induction in order to prove the consistency of PA”
You’ve explained how Gentzen’s proof uses induction up to epsilon_0, but I wonder if it would be helpful to also explain why induction up epsilon_0 is the minimum needed for this kind of proof? As I understand it (based on the discussion in Giaquinto ‘The search for certainty’ p. 192) the argument is that induction up to all ordinals less than epsilon_0 can be proved inside PA. So a proof of consistency using induction up to some ordinal less than epsilon_0 would be formalisable inside PA itself, contradicting Godel’s second theorem (assuming such a proof did not use any other proof techniques lying outside PA).
And here are the typos:
p. 98, end of first para. There’s a comma after the final fulls stop.
p. 99 para. (g) ‘malways’ should be ‘always’
p. 102 para. (c), line 4, ‘contraction’ should be ‘contradiction’
p. 103 final para. line 1, ‘and further’ should be ‘any further’
p. 106, para. C, line 1, ‘Next, Gentzen’s on the consistency of arithmetic’. Should be ‘…Gentzen’s proof of the consistency of arithmetic.’?
I meant to mention this at one point but I don’t think I ever did. Tin Lok Wong, who did his PhD under Richard Kaye in models of arithmetic, has two sets of lecture notes on his website that I think are worth looking at. One is on the consistency of arithmetic blog.nus.edu.sg/matwong/teach/cons/ and one is on models of arithmetic blog.nus.edu.sg/matwong/teach/modelarith/. I would say they are presented at the graduate level, a lot of the material is very terse, but still there is a lot of good exposition and connection of ideas in the sections I’ve read of both. They might be worth looking into as recommendations for the advanced sections on model theory and proof theory.
Many thanks for this! These notes, at a fairly quick glance, do look pretty impressive, and might indeed be worth recommending for Part III.