*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 Godel's first incompleteness theorem 
*(here $T$ is an ["appropriate"](http://dx.doi.org/10.1007/BF02023013) theory of arithmetic.)*:

> 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. [1](https://www.sciencedirect.com/science/article/pii/B9780720422337500253), [2](https://www.jstor.org/stable/2270854), [3](https://link.springer.com/article/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.