This will be a graduate course at the University of Notre Dame.
Course title: Gödel incompleteness
Course description. We shall explore at length all aspects of the Gödel incompleteness phenomenon, covering Turing’s solution of the Entscheidungsproblem, Gödel’s argument via fixed points, arithmetization, the Hilbert program, Tarski’s theorem, Tarski via Gödel, Tarski via Russell, Tarski via Cantor, the non-collapse of the arithmetic hierarchy, Löb’s theorem, the second incompletenesss theorem via Gödel, via Grelling-Nelson, via Berry’s paradox, Smullyan incompleteness, self-reference, Kleene recursion theorem, Quines, the universal algorithm, and much more. The course will follow the gentle treatment of my book-in-progress, Ten proofs of Gödel incompleteness, with supplemental readings.
Hello Joel, your upcoming course sounds very interesting (it is the kind of course I wish I had the chance to take as a student). Recently Albert Visser and I wrote a short paper that includes a new proof of the first incompleteness theorem that only uses Tarski’s theorem; since Tarski’s theorem can be proved with a very straightforward diagonalization that is less tricky than the fixed-point lemma (going back to Tarski himself), it might be of interest to you. The paper is available on arXiv (https://arxiv.org/abs/2311.14025); see Remark 2 of the paper for the pedagogical component.
Thanks for this link—I’ll take a look. I also have been advocating this proof method, and have described it from a few years ago as my favorite proof of incompleteness (https://twitter.com/JDHamkins/status/1468677783505313795, unrolled here: https://threadreaderapp.com/thread/1468677783505313795.html). This proof is a chapter in my forthcoming book on incompleteness, which is the basis of this course. The point I emphasize is that one can prove Tarski’s theorem in an essentially Russellian manner, without any Gödelian self-reference, and this shows how truly very close to Gödel incompleteness Russell was.
Mel Fitting also has an account of this proof method in his article for the Smullyan volume, and he describes Smullyan as emphasizing that much of the fascination people express for Gödel’s theorem is better directed at Tarski’s theorem, and I think he is totally right. (But meanwhile, Mel goes for the sentential version of Tarski, instead of the satisfaction version, and for this reason he has to to internalize the syntax to the object theory. But a simpler proof is possible, avoiding all the internal syntax, if one goes for satisfaction without requiring substitution, as I explain in my book chapter.)
Thanks Joel for your reply and explanations.
Tarski’s theorem that Albert and I use in our paper is the sentential one, and does not refer to models at all, it is the spartan version going back to Tarski that says that if T is a theory in a language L that has the property that the function that maps each unary L-formula phi(x) to phi(#(phi)), where #(phi) is a code for phi, then there is no unary L-formula V(x) such that T proves equivalences of the form psi V(#(psi)) for all L-sentences psi.
As pointed out in the second paragraph of Remark 2 of the paper with Albert, a very special case of Theorem A+ of our paper shows that by using Rosser’s trick and Tarski’s theorem (in the above format) one can prove the first incompleteness theorem in the general form that says for all c.e. consistent extensions of the (very) weak arithmetical theory R (and in particular for all consistent c.e. extensions of Robinson’s Q) are incomplete.
In contrast to the usual proofs of the first incompleteness theorem, due to the bare bones machinery used in the proof, our proof of incompleteness is nonconstructive and does not yield an algorithm such that, given a description of the theory T (that extends R) as input, the algorithm outputs a sentence that is undecidable in T.
Perhaps this simple way of proving the first incompleteness theorem was noticed earlier; given the paramount stature of the incompleteness theorem and the large number of people who have written about it since the 1930s, one would expect for it to have been noticed before; but so far Albert and I don’t know of any. However, after completing our paper we were informed that our proof technique was anticipated by Emil Jeřábek to prove a related result in his MO answer in 2016, (URL: https://mathover
ow.net/q/257044). The latest version on arXiv does include the reference to Emil’s priority in formulating the proof method.
That is very similar to the proof to which I refer. The claim is that in any consistent first-order theory T, of any kind, there can be no definable subset of the plane having every definable unary set as a section, even consistently. I gave a presentation of this argument in my seminar at Oxford in 2021, and a version of the argument appears in section 7 of my recent paper on Fregean abstraction (https://arxiv.org/pdf/2209.07845.pdf). But I also have a short paper on the three views of Tarski, where this is theorem 3. I’ll send you the paper.
But I see now that you are focussed on the sentential version, and so your argument is indeed different than the argument of mine to which I refer. I’ll take a look at your paper as soon as I can.
any chance of seeing these lectures in youtube or edx?
Typo: Entscheidungsproblem has a “c” between the s and the h.
I’m sensitive to that particular c because people are always accidentally leaving it out of my surname. 🙂
I would also love to be able to see this course content anywhere, in any format.
Hello again Joel,
I am writing this note as a way of wrapping up my end of the story it case it proves useful for your course next fall.
In what follows I will refer to the classical 1953 book “Undecidable theories” by Tarski, Mostowski, and (Raphael) Robinson as TMR. A key Theorem in TMR is that any consistent theory that can interpret their theory R (R is a theory even weaker than Robinson’s Q, in contrast to Q, R is not finitely axiomatizable) is essentially undecidable, which immediately implies the first incompleteness theorem for any consistent theory that interprets R. Also, I will use “representable” instead of the more archaic “definable” used by TMR, and will use #(s) for the code of the sentence s.
Theorem 1 (p.46 of TMR) states (in a more modern language) that in any consistent theory T in which the diagonal function is representable , the deductive closure of T (denoted V in TMR) is not representable, in other words, there is no formula F(x) such that for all sentences s we have: T proves F(#(s)) iff T proves S. The proof is very straightforward and uses no magic other than that of Epimenides. In particular, the proof uses a very elementary form of diagonalization, one that is far simpler than the commonly used fixed point lemma, which requires considerable syntactic finesse.
Note that Theorem 1 implies that in particular, there is no formula F(x) such that for all sentences s, T proves F(#(s)) s. So Theorem 1 is a stronger form of the usual way of formulating the sentential form of Tarski’s undefinability of truth theorem.
Theorem 1 plus the theorem that ALL recursive functions can be represented in R immediately yields the essential undecidability of any consistent theory T interpreting R by a one-line argument: the decidability of T implies that V (the deductive closure of T) is representable (since ALL recursive functions are representable). This is basically Corollary 2 on p.49 of TMR. And the essential undecidability of T implies the incompleteness of T in light of the unbounded search that yields the memorable maxim: “every complete c.e. theory is decidable”.
Now here is the punchline: The TMR proof and the one used in my paper with Albert, when applied to proving the basic incompleteness theorem both invoke the the sentential form of Tarski’s undefinability of truth theorem, but in contrast to the TMR proof, which needs one to verify that ALL recursive functions are representable in the consistent c.e. theory T for proving the incompleteness of T, our method only needs (1) the representability of the diagonal function, and (2) the representability of the binary relation “p is a proof of s (in T)”.