In this last (and short!) chapter related to the first incompleteness theorem, we meet ‘Tarski’s Theorem’. And so we arrive at what might be thought of as the Master Argument for incompleteness — for appropriate theories, provability-in-T is expressible in T but truth isn’t, so provability isn’t truth.
Onwards to the second theorem next week!
[Link now removed]
p 102, beginning of §14.3, The inexpressibility of truth —
When applying the Diagonalization Lemma, you say “there will be some LA sentence L such that”, and then in 1, sure enough, there’s ‘L’, but there’s also ‘¬TA’ which hadn’t been introduced. Looking back at the Diagonalization Lemma, I’m thinking ‘¬TA’ is meant to play the role of φ. If that’s right, I think it would be helpful if something made that a bit easier to spot or, alternatively, gave some sort of confirmation that it’s correct.
Compare the proof of Theorem 54 on p 101 where it says “we can apply the Lemma in particular to ¬T(x)”.
One possible rewording:
I would also prefer “depended only” to “only depended”.
Pernickety points:
* You haven’t been using a completely consistent naming convention for the GWT3 files you’ve been giving us, but one thing all the others had in common was that they began with “GWT3_LM”. This one has plain “GWT” instead.
* In the other files, I think you’ve been pretty consistently using a little box to mark the end of a proof; in this one, at the end of p 101, you use a crossed box (which makes me think “don’t tumble dry”).
Good suggestion to have “applies to ¬TA(x)”, thanks.
And I’d forgotten that I needed the plain box later (as in IGT) for a provability operator, and so — to avoid confusion — I will now consistently use crossed box in GWT too to mark the end of proofs!
The short section ends with the paragraph: “How does that statement of Gödel’s square with the importance that he placed on the syntactic version of the First Theorem? Well, Godel was a realist about mathematics: he believed in the real existence of mathematical entities… But that wasn’t the dominant belief among those around him concerned with foundational matters…. the very idea of truth-in-mathematics was under some suspicion at the time. So even though semantic notions were at the root of Godel’s insight, it was extremely important for him – given the intended audience – to show that you don’t need to deploy those semantic notions to prove incompleteness.
Indeed, that helps explain why Gödel emphasized the (much more intricate) syntactic version. But it does not even begin to explain why someone today with no particular qualms about the notion of truth in mathematics should take the same perspective.
I think that there are reasons, but they are quite different. Since the syntactic argument is fully constructive, it gives us a witness for each existential claim made and thus provides more information. That additional information can be useful when seeking spin-offs, elaborations and variants of the basic theorem. For example, the second incompleteness result and the Rosser version are not easily obtained by a simple semantic argument.
Gödel’s realism seems something he invented much later. In 1935, the wrote that quantum mechanics proves Kantian idealism and compared the situation to mathematics (absolute truth = Ding-an-Sich). After his completeness result in 1929, the next objective was completeness of higher order logic for which he needed a truth definition and spoke about this with Tarski in Feb 1930, then saw in May 1930 that completeness fails. Until his meeting with von Neumann in Sept 1930, his proof of incompleteness was based on a crucial result by which “each theorem of the Principia is true,” something he thought had an easy inductive proof by his truth definition. VN suggested he should do it all within arithmetic and Kurt dutifully did so – not much philosophy in that, but a more convincing proof.
Yes, maybe I’ve been too influenced by Feferman’s rational reconstruction. I should probably insert a caveat or two! (Though I guess, at the introductory level of GWT, clearly specifying some positions on the intellectual map is more important than trying to get it right about which historical figure occupied which position when.)
Consider giving a reference to Gödel’s notebooks for the incompleteness result. The image of Gödel as a realist will crumble some time next year when his 1935 quantum mechanics notebooks become available. One piece is called “Fantasizing about the Ding-an-sich!”
Good point — I should make this clear, especially as I go on to get Rosser’s Theorem and the Second Incompleteness Theorem from syntactic arguments!