At Graham Priest's talk for the CUNY set theory seminar yesterday, an issue arose concerning the possibility (or impossibility) of a stronger-than usual form of the arithmetic fixed-point lemma often used to prove the Gödel incompleteness theorem.
The fixed-point lemma, treated in previous MO questions, is commonly described as asserting that for any formula $\varphi(x)$ in the language of arithmetic, with a free variable $x$, there is a sentence $\psi$ such that $PA\vdash\psi\leftrightarrow\varphi({\ulcorner}\psi{\urcorner})$, where ${\ulcorner}\psi{\urcorner}$ denotes the Gödel code of $\psi$. Stronger versions of the fixed-point lemma weaken PA to the theory of Robinson's Q or make the conclusion for more complex webs of fixed points, and these strengthenings are well-known. The fixed-point lemma leads easily to the first incompleteness theorem, since with it one can produce a sentence $\psi$ asserting its own unprovability, and such a statement cannot be provable (or else we would prove something false) and hence is both true and unprovable.
The stronger-than-usual form of the fixed-point lemma desired in the context of one of the speaker's arguments was to find a sentence $\psi$ that was not only provably equivalent to $\varphi({\ulcorner}\psi{\urcorner})$, but was syntactically identical to this assertion. That is, what was needed was what we might call a strong fixed-point, a sentence $\psi$ syntactically of the form $\varphi({\ulcorner}\psi{\urcorner})$.
This appears to be impossible for any of the standard methods of Gödel coding, since for each of these the code ${\ulcorner}\psi{\urcorner}$, as a number, is much larger than the length of $\psi$ as a formula. For example, the code of a sequence of length $k$ is typically much larger than $k$. For such coding, if we understand $\varphi(n)$ to be $\varphi(1+\cdots+1)$, where the substituted term is $n$ many $1$s added, it could never be that $\psi$ is literally the same as $\varphi({\ulcorner}\psi{\urcorner})$, since the latter assertion has length strictly longer than ${\ulcorner}\psi{\urcorner}$, and this is larger than the length of $\psi$. Carl Mummert made a similar point in the latter part of his answer to the MO question mentioned above.
My question is: Is there some method of Gödel coding which would support the strong fixed-point lemma?
And if not, how would one prove such a thing?
Graham suggested that in Gödel's original work, the version of the Gödel sentence produced had the strong fixed-point property, of being literally the same as the assertion that this sentence was not provable.
It occurred to me that if one makes the move beyond what is now considered the usual language of arithmetic $\{+,\cdot,0,1,\lt\}$, for example by adding the function symbols for primitive recursive functions, then one can achieve something very like a strong fixed point. (And perhaps this is close to what Gödel did?)
Theorem. For any formula $\varphi(x)$ with one free variable, there is a closed term $t$ in the language of arithmetic augmented by primitive recursive functions, whose value is precisely ${\ulcorner}\varphi(t){\urcorner}$. Thus, $\varphi(t)$ is a strong fixed point, in the sense that it asserts that $\varphi$ holds of a term whose value is its own Gödel code.
Proof. Let $\text{Sub}(x,y)$ be the primitive recursive function such that $\text{Sub}({\ulcorner}\alpha(x){\urcorner},k)={\ulcorner}\alpha(k){\urcorner}$, substituting $k$ as a term $1+\cdots+1$ in each free occurence of $x$ in $\alpha(x)$. Let $n={\ulcorner}\varphi(\text{Sub}(x,x)){\urcorner}$ and let $t=\text{Sub}(n,n)$, as a syntactic term, using $1+\cdots+1$ to represent $n$. The actual value of the term $t$ can be obtained by evaluating $\text{Sub}(n,n)$, which in light of the definition of $n$, is precisely ${\ulcorner}\varphi(\text{Sub}(n,n)){\urcorner}$, and this is the same as ${\ulcorner}\varphi(t){\urcorner}$, as desired. QED
This lemma essentially provides strong fixed points in the expanded language; but one difference is that we don't have $\psi=\varphi({\ulcorner}\psi{\urcorner})$, where the number is substituted as a term of the form $1+\cdots+1$ of the right length, but rather we have $\psi=\varphi(t)$, where $t$ is a term whose actual value is ${\ulcorner}\psi{\urcorner}$.
Can one prove an analogue of this theorem using terms in the ordinary language of arithmetic $\{+,\cdot,0,1,\lt\}$?
