July 8, 2018


Kurt Gödel and the mechanization of mathematics (JULIETTE KENNEDY, TLS Online)

[G]ödel showed that truth and provability cannot be identical, because one concept is definable, while the other is not. Perhaps it should come as no surprise that mathematical truth, which has to do with objectivity and existence, is not the same thing as the concept of formal proof, which has to do with evidence and justification.

Gödel knew that because of the anti-metaphysical bias in the air at the time, mainly emanating from the so-called Vienna Circle, which he attended from time to time, logicians would not have accepted his proof, given that the concept of truth, together with its undefinability, played such a central role in it. So Gödel published neither this first proof of the incompleteness theorem nor the theorem on the undefinability of truth, only speaking of them many years later - a remarkable show of restraint, given the importance of those theorems.

Here now is a sketch of the proof of the First Incompleteness Theorem that Gödel published in 1931. The definability of provability played a role in Gödel's original proof, as I sketched above, as did self-reference. The phenomenon of self-reference can be harmless, as when one says of oneself, that one is thirsty. But it can also create paradoxes in natural language, the most notable of which is the Liar's Paradox.

To see this, consider the natural language sentence S, where S stands for: "This sentence is false".

S is self-contradictory. For if S is true then what it says about itself must be the case: it is false. On the other hand, if S is false then what it says of itself, namely that it is false, is true. This shows that S is true if and only if it is false. Or in technical terms, that S has no truth value.

With arithmetization, Gödel was able to express the Liar's Paradox in Peano arithmetic, but with provability in place of truth, to wit: "This sentence is unprovable" rather than "This sentence is false".

It is very striking that with such an apparently trivial device, namely the encoding of syntax, one could prove such a devastating theorem. In fact, Gödel wondered about this himself, referring to his proof as a "parlour trick" in conversation with the logician Georg Kreisel.

Even more striking is the fact that Gödel held to his rationalistic view of mathematics (and of philosophy) throughout his life, even in the face of his own theorems. "As to [mathematical] problems with the answer Yes or No," he said in the 1930s, "the conviction that they are always decidable remains untouched by these results." Decidable by humans, that is, using methods that transcend any given finite set of computational rules.

Posted by at July 8, 2018 11:13 AM