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 Entsheidungsproblem, 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?