Where did this presentation of Gödel's theorem appear?

Question

This question was asked and bountied at MSE, with no response.

---

Many years ago I ran into the following proof of Gödel's first incompleteness theorem (here $T$ is an "appropriate" theory of arithmetic; see Jones and Shepherdson - Variants of Robinson's essentially undecidable theory $R$):

First, we observe that Tarski's undefinability theorem can be slightly tweaked to say that for all $M\models T$, the theory of $M$ can't be the standard part of an $M$-(parameter-freely-)definable set. Next, by the usual representability arguments we have that every computable set is invariantly definable: if $X\subseteq\mathbb{N}$ is computable and $M\models T$ then $X$ is the standard part of a definable set in $M$. Now if $S$ were a computable satisfiable completion of $T$ we would get a contradiction by looking at $M\models S$. If we want, we can then replace "satisfiable" with "consistent" via the completeness theorem.

My question is:

Where did this argument appear?

I'm not asking whether this is a "genuinely different" argument (although that said, see here). Rather, I'm interested in its presentation in terms of invariant definability. This was a notion first introduced by Kreisel following Godel/Herbrand and subsequently studied by others (see e.g. Kreisel - Model-theoretic invariants: Applications to recursive and hyperarithmetic operations, Moschovakis - Abstract Computability and Invariant Definability, Apt - Inductive definitions, models of comprehension and invariant definability). My vivid recollection is that the argument above appeared as a footnote in the first paper mentioned above, but it turns out it's not there after all.

Answer 1

This argument is essentially similar to the argument of Mel Fitting in his article, "Russell's paradox, Gödel's theorem" Chapter in book: Raymond Smullyan on self reference, 47–66, Outstanding Contributions to Logic, 14, Springer, Cham, 2017.

We had used this article as one of the readings in my Graduate Phil Logic seminar last term.

Fitting argues via Russell's paradox using Tarski's theorem on the non-definability of truth, in a manner that I find very similar to the argument you describe (although he doesn't use your invariant terminology, and perhaps you may regard his argument as not the same as what you intend). Namely, he argues that although provability is representable, truth is not, because of Russell's theorem, and so the incompleteness theorem follows.

Part of his point in that article is that this way of arguing avoids the need for explicit self-reference.

Answer 2

EDIT: I think I finally figured it out! At around the same time that I was reading Kreisel's invariant definability paper, I was also looking at Kikuchi/Tanaka, On formalization of model-theoretic proofs of Godel's theorems for completely different reasons. This paper goes into careful detail on internal model-constructions, and in particular Corollary 5.6 has a very "modal" feel to it (if $\mathfrak{M}_0$ can "see"/build according to a specific type of procedure $\mathfrak{M}_1$, then we get $\Sigma_1$-persistence from $\mathfrak{M}_0$ to $\mathfrak{M}_1$). I think while trying to understand the details of the K/T paper I noticed the (to me anyways) affinity with invariant definability ideas.

---

Based on the lack of reference provided here and at MSE, as well as my own lack of success in finding a reference, I'm going to tentatively say that this particular approach has not appeared as such in print. I'll delete this answer of course if someone supplies a reference in which it appears, but I think at present it's appropriate to move this off the unanswered queue (I've made my answer CW since the line between answer and non-answer here is a bit blurry, so this doesn't feel quite right as a reputation-producing answer).

---

Very belatedly, in response to Joel's answer: I see a meaningful difference between Fitting's argument and the one in the OP - which I'll call "Kreiselian" - due to the former's reliance on representability of provability. (For simplicity, below I'll conflate sentences/formulas with their Godel numbers and leave some things unoptimized.)

Consider the following (basically the "right" conclusion of the Kreiselian argument, while staying in the realm of arithmetic for simplicity):

$(\star)\quad$ Suppose $\mathfrak{C}$ is a class of models of Robinson's $\mathsf{R}$ with $\mathbb{N}\in\mathfrak{C}$. Then there is no complete theory $T$ in the language of arithmetic such that

• $T$ is "$\mathfrak{C}$-satisfiable" (= some $\mathcal{M}\in\mathfrak{C}$ satisfies $T$) and

• $T$ is "$\mathfrak{C}$-invariantly-definable" (= there is a formula $\varphi$ such that $\varphi^\mathcal{N}\cap\mathbb{N}=T$ for every $\mathcal{N}\in\mathfrak{C}$ - here I'm conflating sentences with their Godel numbers for simplicity).

Fitting's argument can be summarized as "provability is representable but truth is not." In the system-of-structures framework provability corresponds to the common theory of the class $\mathfrak{C}$ under consideration, and so Fitting's argument proves $(*)$ in the special case that $\mathfrak{C}$'s common theory is not too complicated. But no such assumption is needed for the Kreiselian argument.

Of course, the generality of $(\star)$ doesn't seem to have any use - I don't know of any interesting applications where the system $\mathfrak{C}$ is not reasonably nice, with better arguments thus applying. But this is at least a mathematically meaningful statement which Fitting's argument, unless I'm missing something, doesn't yield.