Peter Smith's Blog, page 51

Gödel Without Tears, not quite the end

I was intending to post Chapter 17 today — the final chapter, dealing with Löb’s Theorem and related results. But looking again at my draft version yesterday, I thought it was/is rather a mess, and that some of the material is even in the wrong chapter. So some not-quite-trivial rewriting is needed. It will be a day or two before I can get down to doing that.

Meanwhile, many thanks to all those (some here, more by email) who have sent corrections and comments and suggestions about earlier chapters. I’ll try to get a revised version of the whole thing, plus suggestions for further reading, and an index, done by the middle of next month. And then delight the world with another Big Red Logic Book …

The post Gödel Without Tears, not quite the end appeared first on Logic Matters.

Gödel Without Tears, slowly, 16

Today’s chapter is optimistically entitled ‘Proving the Second Incompleteness Theorem’. Of course we don’t actually do that! But we do say something more about what it takes to prove it (stating the so-called derivability conditions, and saying what it takes to prove them).

As an extra, we say how it can be that there are consistent theories which ‘prove’ their own inconsistency.

The post Gödel Without Tears, slowly, 16 appeared first on Logic Matters.

Gödel Without Tears, slowly, 15

[I’ve retitled the previous post, to keep blog post numbers in sync with chapter numbers!]

We at last move on to the Second Theorem. In Chapter 15, we introduce the theorem, and explain its significance for Hilbert’s programme. This involves a  cartoon history trying to bring out the attractions of Hilbert’s programme (surely one of the great ideas in the philosophy of maths — if only it had worked!).

 

 

 

The post Gödel Without Tears, slowly, 15 appeared first on Logic Matters.

Gödel Without Tears, slowly, Interlude

Today’s short episode is a second ‘Interlude’, separating the chapters on the first incompleteness theorem from the final three chapters on the second theorem. But it mentions (or at least, gestures at) enough interesting points for it to be worth its own post.

[There a reference to a Theorem 51, which is the previously unnumbered result — now indeed to be recognized as a theorem in its own right — at the end of §13.3. which says that if a theory T is p.r. axiomatized and contains Q, the formal predicate ProvT does not capture the property of being a T-theorem.]

The post Gödel Without Tears, slowly, Interlude appeared first on Logic Matters.

Gödel Without Tears, slowly, 15

Today’s short episode is a second ‘Interlude’, separating the chapters on the first incompleteness theorem from the final three chapters on the second theorem. But it mentions (or at least, gestures at) enough interesting points for it to be worth its own post.

[There a reference to a Theorem 51, which is the previously unnumbered result — now indeed to be recognized as a theorem in its own right — at the end of §13.3. which says that if a theory T is p.r. axiomatized and contains Q, the formal predicate ProvT does not capture the property of being a T-theorem.]

The post Gödel Without Tears, slowly, 15 appeared first on Logic Matters.

Lea Desandre sings Monteverdi and more …

Twenty minutes of delight and balm for the soul: Lea Desandre singing with Thomas Dunford and members of Les Arts Florissants.

The post Lea Desandre sings Monteverdi and more … appeared first on Logic Matters.

Gödel Without Tears, slowly, 14

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!

The post Gödel Without Tears, slowly, 14 appeared first on Logic Matters.

Gödel Without Tears, slowly, 13

We get today to Chapter 13, called ‘The Diagonalization Lemma, and Rosser’s Theorem’. Not that we actually prove Rosser’s theorem in detail, as this is fiddly. But I do establish the Lemma, show how it can be used to derive the syntactic version of the first theorem again, and I indicate the key construction for getting to Rosser’s theorem.

(Looking back at Chapter 12, though, I see that the section which actually proves the first theorem there had become rather oddly arranged: I’ve rearranged a bit, separating out the theorem from a couple of corollaries worth remarking. So I’ve included a revised Chapter 12 too.)

The post Gödel Without Tears, slowly, 13 appeared first on Logic Matters.

Gödel Without Tears, slowly, 12

And, at last ….

Cue drumroll …

‘The First Incompleteness Theorem, syntactic version’

This is the version of the theorem that Gödel highlights in his epochal 1931 paper, and which people usually have in mind when they talk of ‘the’ incompleteness theorem. We have to do a little  more work than for the semantic version, but again — once we have grasped the trick of constructing a Gödel sentence, and understood the idea of capturing/representing/defining primitive recursive relations in a formal theory, the proof is delightfully simple. Which is not to diminish  Gödel’s achievement in the slightest: on the contrary, it was very important to him that the ideas involved are straightforward to handle once you grasp them.

The post Gödel Without Tears, slowly, 12 appeared first on Logic Matters.

Gödel Without Tears, slowly, 11

And at last, we get to a proof of ‘The First Incompleteness Theorem, semantic version’, uisng pretty much Gödel’s materials. And given our background work over previous chapters, it is very easy. Grasp the trick in constructing the described Gödel sentence, and everything then falls speedily and simply into place. Enjoy!

The post Gödel Without Tears, slowly, 11 appeared first on Logic Matters.