I think that the best way to capture the idea beyond the proof of the
fixed point theorem is to mirror it in an ordinary language
formulation and then translate it back to the first order language of
arithmetic (cf. J.N. Findlay, Goedelian Sentences: A Non-numerical
Approach}, Mind, Vol. 51, 1942, pp. 259-65.). Clearly,
what we seek is a sentence asserting that it has a given property,
that is, a sentence that says "I have the property p". But,
in order for it to be formalizable, our sentence should consist of
components with easily identifiable formal first-order
counterparts. Therefore we cannot use such indexicals as `I'.

In order to circumvent the need for indexicals, we reformulate
Grelling's paradox applying it to open sentences instead of
adjectives:

(1) "x is heterological" is heterological,

where an open sentence is called autological if the property it
attributes to x possessed by the sentence itself, otherwise it is called
heterological. For example, "x consists of five words", "x is
English", are autological, while "x is long", "x is German", are
heterological. On the other hand, both in formal languages and in informal
ones, the fact that an object has a property is expressed by a
substitution of the name of the object into the open sentence
expressing that property. Consequently,

(2) x is heterological just in case the sentence obtained by
substituting the name of x for the variable in it is false.

Now (using the convention that he name of linguistic objects are the
object itself between quotation marks), if we replace "being false" by
"having property p", (1) and (2) together yield:

(3) the sentence obtained by substituting the name of
"the sentence obtained by substituting the name of
x for the variable in it has property p"
for the variable in it has property p.

**This is the sentence we need.** On the one hand, it does not use indexicals, on the other, it indeed says of itself
that it has property p (and says nothing else), since it is built up in
such a way that if we perform the substitution described in it, then
we obtain the sentence itself, which is stated to have property p.

Now, let s denote the open sentence between the quotation marks
in (3), that is, let s be:

(4) the sentence obtained by substituting the name of
x for the variable in it has property p.

Then, clearly, the whole sentence (3) is s("s"). In order to obtain
the fix point lemma, we should translate it into the language of formal
arithmetic. Clearly, the formalization process consists of two main steps. In the first step, we have to find the formal version $\eta$ of s, and then the second step is obvious: the desired sentence $\lambda$ will simply be $\eta(g(\eta))$ (where $g(\varphi)$ is the G\"odel number of $\varphi$ and plays, of course, the formal counterpart of name of $\varphi$, and, for simplicity, I leave out of consideration the difference between numbers and their formal counterparts in the language).

Now, that is all. That is the essence of the proof. What remains to do
is simply translate the ordinary language argument into
the formal language of arithmetic. That is a completely mechanical task.

Let us recall that what we should show is that,
for any arithmetical formula $\varphi$ with at most one free
variable (this fact will be denoted by $\varphi=\varphi(x)$), there is a sentence $\lambda$ such that

$Q\vdash \lambda \longleftrightarrow
\varphi(g(\lambda)),$

where $Q$ is Robinson arithmetic (essentially Peano arithmetic without induction).

Now, let the formula corresponding to the property p be $\varphi=\varphi(x)$. Then, obviously, the formal version of s is
$\varphi(g[x(g(x)])$. In order to continue the formalization process,
we should find a formula that can play the role of
$\varphi(g[x(g(x))])$, that is, a formula $\eta=\eta(x)$ such that
$\eta(g(\psi))$ is provably equivalent to $\varphi(g[\psi(g(\psi))])$
for every $\psi=\psi(x)$, or equivalently (denoting the inverse of $g$
by $g^{-1}$), for any $n \in N$,

$Q\vdash \eta(n)\longleftrightarrow\varphi(g[g^{-1}(n)(n)]). $

In order to find the appropriate formula $\eta$,
let us consider the expression
substituted into the formula $\varphi$,
and define the function $f:\omega\longrightarrow \omega$ accordingly:

$f(n)=g[g^{-1}(n)(n)]$ if $n \in N$ and $f(n)=0$ otherwise.

Since this function is obviously recursive and hence representable,
and, up to provable equivalence, the result of substituting a
representable function into a formula can also be expressed by a
formula, there is a formula $\eta$ such that, for any $n\in N$,

(5)
$Q\vdash\eta(n)\longleftrightarrow\varphi(f(n))$

Thus we have obtained what we need, we have shown that there exists an
$\eta$ that can be considered to be the formal version
of s. Now, all that remains to do is straightforward:
it follows from (5) that, for every $\psi$,

$Q\vdash \eta(g(\psi))\longleftrightarrow
\varphi\big(g[\psi(g(\psi))])$,

which, in turn, choosing $\psi$ to be $\eta$, yields

$Q\vdash \eta(g(\eta))\longleftrightarrow
\varphi(g[\eta(g(\eta))])$,

showing that the sentence
$\lambda =\eta(g(\eta))$ indeed has the desired
property.

Naming and Diagonalization, from Cantor to Gödel to Kleenefor insight about the common theme between various diagonalization theprems, including Carnap's [the arithmetic fixed point theorem is due to him, according to Gaifman]. Here is the link for Gaifman's paper: columbia.edu/~hg17/naming-diag.pdf $\endgroup$1more comment