*This question was asked and bountied [at MSE](https://math.stackexchange.com/questions/3578756/where-did-the-language-in-this-proof-of-godels-incompleteness-appear), 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$](http://dx.doi.org/10.1007/BF02023013))*:



> 
> 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](https://mathoverflow.net/a/353900/8133))*. 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](https://doi.org/10.1016/B978-0-7204-2233-7.50025-3), [Moschovakis - Abstract Computability and Invariant Definability](https://doi.org/10.2307/2270854), [Apt - Inductive definitions, models of comprehension and invariant definability](https://doi.org/10.1007/BF02762011))*. 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.



Where did this presentation of Gödel's theorem appear?
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*](https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-35/issue-3/On-Formalization-of-Model-Theoretic-Proofs-of-G%c3%b6dels-Theorems/10.1305/ndjfl/1040511346.full) 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.


