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

Many years ago I ran into the following proof of Godel's first incompleteness theorem (here $T$ is an "appropriate" 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). 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, 2, 3). 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.