I mentioned a couple of days ago that, in the last four months, the newly available PDFs of my *Intro to Formal Logic *and *Intro to Gödel’s Theorems *have both been downloaded over 3.5K times (and that’s ignoring an initial flurry of downloads of the Gödel book by people who clicked on a probably misleading link posted elsewhere). In the same period — without any advertising at all — the *Teach Yourself Logic Study Guide* has been downloaded 7.5K times. I mention this to explain again why I feel I ought to give the *TYL* project some love and spend some quality time updating the *Guide*: if it is being downloaded that much, with a big surge at the beginning of semesters, it must be being recommended as useful. So I guess I really ought to make sure it is as useful as it can be, and indeed make sure it reflects what I now think about which texts to recommend. The last full version was a pretty rough-and-ready layered accumulation of bits and pieces of various vintages: it is well past time for an end-to-end rewrite. But heavens, it’s necessarily a slow job, as I revisit texts old and new!

Anyway … here now is the latest version of the new-style Guide up to the rewritten Chapter 6. This reworked chapter covers three inter-connected topics: (a) the elementary informal theory of arithmetic computability, (b) an introduction to formal theories of arithmetic and how they represent computable functions, which leads up to (c) Gödel’s epoch-making incompleteness theorems

My reading recommendations for this chapter haven’t changed a lot. But a feature of the revised Guide is that (after the preliminary chapters), each chapter has a section (or two) giving an extended overview of its theme, from five to ten pages long. These overviews are supposed to be elementary indicators of some of the topics covered by the recommended reading. They can certainly be skipped (that’s clearly signalled): the overviews are included just for those who might find this kind of preliminary orientation helpful. It is difficult to know just how to pitch them, and I will no doubt later revisit the set of overviews to make them more uniform in style and level (so comments appreciated!).

I realize now that the *Teach Yourself Logic Study Guide *has been so-called for over eight years. Maybe I shouldn’t change the “brand” name after all ….

RichardI think it could be helpful to have a small section on sources that treat the second incompleteness theorem in detail. I know most texts skip the proofs of the Hilbert-Bernays-Lob derivability conditions because they are boring and tedious. But for readers who *do* want to see those details, it could be helpful to list a few places where they can be found.

On a related point, “Godel’s Theorems and Zermelo’s Axioms” by Lorenz Halbeisen and Regula Krapf is a new book that claims to give a full proof of the second incompleteness theorem, though I haven’t read it myself yet.

Peter SmithIs there a source at a level of accessibility comparable to the other recommendations in Chapter 6? I’ll check again but I think not [I’ve skimmed the first half of Halbeisen and Krapf and wasn’t at all impressed, but I’ll see what they do with the Second Theorem].

Maybe what I should do is, yes, explicitly note that the Second Theorem isn’t fully proved in the books mentioned here, and then give a pointer forward to the chapter with more advanced readings in the [yet to be re-written!] Part III of the Guide.

RichardThe pointer to Part III sounds like a good idea.

The only modern sources I can think of that cover the second incompleteness theorem in detail are Tourlakis vol. I (as Rowsety Moid mentioned), Rautenberg, and the new Halbeisen & Krapf book. But perhaps these are best saved for a later chapter.

Peter SmithThere’s Boolos’s provability logic book as well — whose treatment is perhaps more accessible than most?

Rowsety MoidLectures in Logic and Set Theory: Volume I: Mathematical Logic: Volume 1, Mathematical Logic, by George Tourlakis, looks like it has a proof of the second theorem.Peter SmithYes, and the last chapter of Rautenberg. I’ll have another look at both as supposedly written at a relatively accessible level. But as I recall, Rautenberg is rather relentlessly compressed.

Ana AmorimProfessor Smith,

I have been using your guide to teach myself logic, and it was a lifesaver, a fantastic little book. I’m interested in legal logic (deontic logic applications in law), and I followed your reading recommendations.

As someone coming from a social science background, I would like to suggest a more detailed treatment of math requirements. Set theory, relations, functions, structures are essential topics, and maybe you could emphasize that.

How to prove, by Velleman, is a good start, but I found out that More Precisely, by Steinhart, although great, isn’t enough. I’ve read Enderton’s Set Theory, and I think it is essential reading. Douglas Smith’s “A transition to Advanced Mathematics” and Joel Hamkins’ Proof and the Art of Mathematics are both nicely illustrated and very useful for beginners. Another lovely book is The Foundations of Mathematics, by Ian Stewart and David Tall. Kevin Houston’s Ηοw to think like a mathematician talks about how to read theorems and proofs, and it is beneficial as well.

Peter SmithThanks for this. I think there are two good points here.

First, on adding one or two things alongside Velleman’s

How to Prove It, to help ease in the non-mathematical reader: I’ve Joel Hamkins’s book on the desk here as I write, and I need to take a proper look at it, but it could indeed be just the thing.Second, as you say, basic ideas about sets, relations, functions, cardinalities, etc — i.e. VERY basic set theoretic ideas (some of what’s often called “naive” set theory) — should probably be encountered early, before tackling a full-on (even if still elementary) treatment of set theory. When thinking about what would be the next chapter of the Guide on (relatively elementary) set theory, I’ve already been turning over in my mind the idea of in fact separating out such naive set theory, and having a short chapter on that earlier in the Guide.

David AuerbachBack in the day, the young me benefited enormously from Russell’s Introduction to Mathematical Philosophy and I always think of books like those mentioned above as modern updates of his.

Ana AmorimThank you, Professor.

I learned a lot from discrete math books. I liked Susanna Epp’s Discrete Mathematics with Applications. She gives clear explanations and provides detailed proofs. For beginners, it’s hard when books omit a step.

Stanford CS 103 course notes (and the additional material) is very clear and easy to understand (http://web.stanford.edu/class/archive/cs/cs103/cs103.1184/notes/Mathematical%20Foundations%20of%20Computing.pdf)

There are some great video lectures on You Tube. I wasn’t a great fan of video lectures, but I watched videos about set theory and changed my opinion.

Trefor Bazett’s discrete math course has several short lessons on sets, relations and functions (https://youtube.com/playlist?list=PLHXZ9OQGMqxersk8fUxiUMSIx0DBqsKZS).

MIT’s Math for computer science is another option, but it’s more rushed than Bazett’s (https://youtube.com/playlist?list=PLUl4u3cNGP60UlabZBeeqOuoLuj_KNphQ).

Finally, I really enjoyed this [playlist](https://youtube.com/playlist?list=PLztBpqftvzxWUF1psif8R7aUph4tsIuNw).

Francis Leeabout the second incompleteness theorem:

【I】there are a lot of ‘partial proofs’ of the classical form of GIT2 (I prefer Girard’s)

carried out in PA:

Boolos – The logic of Provability

Felscher vol3

Rautenberg

Hinman

Monk

Grandy

Tourlakis vol1

Feferman 1960

Halbeisen & Krapf

[carried out in PRA]

Girard – Proof Theory and Logical Complexity I

Smorynski – Self Reference and Modal Logic

I can’t recommend Tourlakis’s book, though. In the preface He said something like ‘PRA is stronger than PA’ (but everyone knows that PRA is weaker than PA, isn’t it?)

and I think, the cannonical proof of GIT2 should be carried out in PRA.

【II】the modern version (proof theoretical version) of GIT2:

Here’s a good survey article:

Yong Chen ‘Current research on Godel’s incompleteness theorems’

https://arxiv.org/abs/2009.04887v2

see especially corollary 5.4

related works:

Pudlak 1985 ‘Cuts, Consistency Statements and Interpretations’

Visser 2011 ‘Can We Make the Second Incompleteness Theorem Coordinate Free’

Peter SmithThanks …that’s a very useful checklist!

Rowsety MoidIt’s occurred to me that there’s something in the vicinity of the 2nd incompleteness theorem that isn’t quite clear in GWT or IGT.

Here it is in GWT, p 113:

And here it is in IGT, p 239

I’ve seen similar points in other places as well. But what exactly are they saying? Put another way, which impossible possibilities are they meant to cover?

If (1) we’re told (by divine revelation, say) that there’s a T-proof of T’s consistency, then, sure,

thatdoesn’t help us, because T might be inconsistent and the proof might exploit that inconsistency.But what if (2) we prove that there’s a T-proof of T’s consistency — merely that one exists, without exhibiting the actual proof — and our proof that the proof exists does not exploit any inconsistency in T? Some ways of doing that wouldn’t help, because the consistency proof might exploit an inconsistency in T even though the proof that it existed didn’t. But what if the existence proof ruled that out?

Or, even better, what if (3) we exhibit an actual T-proof of T’s consistency, where that consistency proof doesn’t exploit any inconsistency in T? That

Tis inconsistent means there’s at least one proof; it’s not what gives us the proof we’re exhibiting.The reason I’m talking about exploiting an inconsistency is that at least the usual ways to show we can derive anything in an inconsistent theory use the inconsistency when giving the general form of the proofs of arbitrary things. But the inconsistency doesn’t necessarily contaminate all proofs. (Suppose I ask a friend to write down a false arithmetic statement — call it

?— and seal it in an envelope I never open, so that I don’t know what?is; and then I usePA+?. All of my proofs in or aboutPA+?will be exactly as if they’d been in or about plainPA, or at least they won’t use the inconsistency in any significant way.) (Or let’s say I don’t even know?is false.)