Question

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.

It can directly be checked that this

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"). That isIn order to obtain the fix point lemma, we should translate it into the language of formal arithmetic. Clearly, the formalization process should consist 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.