The previous chapter gestured towards a proof of incompleteness which relies on constructing a Gödel sentence which is true if and only if it is unprovable. This proof idea is ingenious. Too ingenious? Some, when they first encounter it, worry that an illegitimate trick is being played.

That’s wrong, as hopefully will become quite clear in later chapters. It might help, though, to counter any temptation to think that there’s something fishy about the incompleteness theorem if we pause to look at a different sort of proof — one that *doesn’t* depend on the construction of a tricksy Gödel sentence.

Chapter 4, ‘Undecidability and incompleteness’, therefore gives a lovely proof which I first learnt from Timothy Smiley a very long time ago. The argument is one of my favourite ones in all logic — it’s so elegant and easy to understand that every student should know it!

Sam ButchartI think the final sentence of para. 5 on the first page has got garbled: “And as we will later see that it is …” is a blend of “And as we will see later it is …” and “And we will see later that it is…”

I also think using ‘captures’, with its mnemonic, is pedagogically much better than “represents”. I clearly remember when I was first learning about these things, never being able to remember which was which with “expresses” and “represents”. Even without the mnemonic, “capture” has more of a feeling of syntactic provability about it.

Theorem 7 is indeed very lovely. Will people understand what you mean by calling it a non-trivialisation result? Some might wonder why an area of mathematics which can be axiomatised in a decidable theory would be ‘trivial’. This is the mathematician’s sense of ‘trivial’ I suppose, meaning something like not very deep or difficult or interesting, mathematically speaking. Maybe that needs a little elaboration?

Peter SmithThanks for this. Yes, the “trivialisation” remark is probably too brisk, and needs expanding just a little.

Rowsety MoidI think this is a very helpful chapter, and not only for calming fears about self-reference.

It also, I think, at least helps to addresses another worry, that the Godel sentence for T doesn’t connect to T-provability in the way it would need to.

At the end of §3.6, it says it’s ‘stretching a point’ to say the G for T says ‘I am unprovable in T’ and that it doesn’t really say that. Yet shortly after, in the proof of Theorem 1 in §3.7, we read that it ‘is true iff it is not provable’. And in §3.8, we read that GT is is equivalent to “‘GT’ is not probable in T”. In the intro paragraphs of chapter 4, we read the the sentence “in effect ‘says’

I am not provable in T“. How does all that fit together?Anyway, the proof via D in chapter 4 doesn’t get entangled in the same difficulties and so might provide a model for presenting / understanding Godel’s approach.

(I don’t know how to get the T in GT to appear as a subscript.)

*

p 21, reality check and footnote 1:

I think there’s an issue here that can also happen in other cases when trying to make it clear that / why two similar-looking pieces of terminology are different (the two sorts of completeness, for example).

Reading the parenthesised reality check, it’s clear the two notions are different. There are quit a few differences, though, at least in the way the two notions are explained. The explanation of ‘T is decidable’

— is about T and arbitrary sentences

— is about whether there’s a mechanical procedure

— is about being a ‘theorem’

— uses the notation ‘T |- φ’

— does not mention not-φ

The explanation of ‘T decides’

— is about T and a single sentence

— is about what T ‘proves’

— does not use ‘theorem’

— does not use the notation ‘T |- φ’

— says ‘either φ or not-φ’

Which difference is the key difference? How much do the other ones matter? Which ones are real differences rather than incidental differences in wording?

The footnote is helpful. Is this way of putting things together correct?

When a theory T is decidable, there’s a mechanical procedure that, given any sentence φ in T’s language, tells you whether T proves or doesn’t prove φ. If T decides φ, and T is decidable, the mechanical procedure says ‘yes’ either for φ or for not-φ; when T doesn’t decide φ, the procedure says ‘no’ for both φ and not-φ.

I’m thinking ‘T proves φ’, ‘φ is a theorem of T’, and ‘T |- φ’ are different ways to say the same thing. Is that correct?

*

Other things:

I’m not sure that just (only) saying ‘a truth-table test’ is the best way to explain why the the toy propositional theory T of §1.3 is decidable. §1.3 doesn’t say anything about truth-table tests. It says “T has a complete logic, since standard propositional calculi are complete.”

Wording issue: in the footnote, I think it should be ‘decide q’ rather than ‘decide whether q’. The ‘whether’ phrasing goes better with cases like ‘whether T |- φ’; you haven’t normally used it for plain ‘decides’. For example, near the top of the page you have ‘T formally decides a sentence φ’.

(Minor issue: is this sort of thing really a reality check? A reality check is normally about checking against the real world, or at least something more concrete. This is more a terminology check, or something like that.)

*

p 22 ‘captures’ vs ‘represents — I strongly prefer ‘captures’. ‘Represents ordinarily has a meaning very like that of ‘expresses’.

Peter SmithFirst point: it was misleading for me to write ‘is equivalent to’ when no more “if and only if” was meant. And yes, some other minor rephrasing would improve.

Second point: sure, ‘T proves φ’, ‘φ is a theorem of T’, and ‘T |- φ’ are different ways to say the same thing. The first two by §1.2 (ii); the first and third by Defn 4. I could add “equivalently, φ is a theorem” to that definition.

As to decides/decidable, I’m not sure I need to say more. Though I do like your suggested “Terminology check”!

Final point: yes, that’s exactly the reason I prefer “captures”.

Rowsety MoidSo, to be clear: since ‘T proves φ’, ‘φ is a theorem of T’, and ‘T |- φ’ are different ways to say the same thing, describing ‘decidable’ using ‘theorem’ and ‘T |- φ’, but ‘decides’ using ‘proves’, creates differences that are incidental differences in wording, which can make it harder for the reader to pick out the difference that matters.

Peter SmithOK! Point taken, thanks.