I want to understand the idea of the proof of the artihmetic fixed point theorem. The theorem is crucial in the proof of Gödel's first Incompletness theorem.


First some notation: We work in $NT$, the usual number theory, it has implemented all primitve recursive functions. Every term or formula $F$ has a unique Gödel number $[F]$, which encodes $F$. If $n$ is a natural number, the corresponding term in $NT$ is denoted by $\underline{n}$. The function $num(n):=[\underline{n}]$ is primitive recursive. Also, there is a primitive recursive function $sub$ of two variables, such that $sub([F],[t])=[F\_v(t)]$, where $v$ is a free variable of $F$ which is replaced by a term $t$.


Now the theorem assertions the following:



> 
> Let $F$ be a formula with only one free variable $v$. Then there is a sentence $A$ such that $NT$ proves $A \Leftrightarrow F\_v(\underline{[A]})$.
> 
> 
> 


This may be interpreted as a self-referential definition of $A$, which is, as I said, crucial in Gödel's work. I understand the proof, I just repeat it, but I don't get the idea behind it:


Let $H(v)=F\_v(sub(v,num(v)))$ and $A = H\_v(\underline{[H]})$. Then we have


$A \Leftrightarrow H\_v(\underline{[H]})$
$\Leftrightarrow F\_v(sub(v,num(v)))\_v(\underline{[H]})$
$\Leftrightarrow F\_v(sub\_1(\underline{[H]},num(\underline{[H]})))$
$\Leftrightarrow F\_v(sub\_1(\underline{[H]},\underline{[\underline{[H]}]}))$
$\Leftrightarrow F\_v(\underline{[H\_v(\underline{[H]})]})$
$\Leftrightarrow F\_v(\underline{[A]}), qed.$


But why did we choose $H$ and $A$ like above?



Arithmetic fixed point theorem
The fixed point lemma is profound because it reveals a
surprisingly deep capacity in mathematics for
self-reference: when a statement $A$ is equivalent to
$F(A)$, it effectively asserts "$F$ holds of me". How
shocking it is to find that self-reference, the stuff of
paradox and nonsense, is fundamentally embedded in our
beautiful number theory! The fixed point lemma shows that
every elementary property $F$ admits a statement of
arithmetic asserting "this statement has property $F$".


Such self-reference, of course, is precisely how Goedel
proved the Incompleteness Theorem, by forming the famous
"this statement is not provable" assertion, obtaining it
simply as a fixed point $A$ asserting "$A$ is not
provable". Once you have this statement, it is easy to see
that it must be true but unprovable: it cannot be provable,
since otherwise we will have proved something false, and
therefore it is both true and unprovable.


But I have shared your apprehension at the proof of the
fixed point lemma, which although short and simple, can
nevertheless appear mysteriously impenetrable, like an
ancient mystical rune that we have memorized. We can verify
it step-by-step, but where did it come from?


So let me try to explain how one could derive this
argument, or at least arrive at it by small steps.


We want to find a statement $A$ that is equivalent to
$F(A)$. If we could expect a strong version of this, then
we would seek an $A$ that is equivalent to $F(A)$, and to
$F(F(A))$, and so on, expanding from the inside. Such a
process leads naturally to the infinitary expression


* $F(F(F(\cdots)))$


Furthermore, this infinitary expression is itself a fixed
point, in a naive formal way, since if $A$ is that
expression, then applying one more $F$ results in an
expression with the same form, as desired. This infinitary
expression doesn't count as a solution, of course, since we
seek a finite well-formed expression, but it suggests an
approach.


Namely, what we want to do is to capture in a single finite
expression the self-expanding nature of that infinitary
solution. The desired statement $A$ should be equivalent to
the assertion that $F$ holds when substituted at $A$
itself. So we introduce an auxiliary variable $v$ and
consider the assertion $H(v)$ that asserts that $v$ is as
desired, namely, that $F$ holds of the statement $v$ codes,
when substituted at $v$. This last self-substitution part,
about substituting $v$ at $v$, is what allows one
substitution to self-expand into two, and then three and so
on, in effect curling the self-expanding infinite tail of
the infinitary expression around onto itself.


Namely, if $n$ is the code of $H(v)$, then we perform the
substitution, obtaining the statement $H(n)$, which
asserts exactly that $F$ holds of the statement $n$ codes
when substituted at $n$. But since $n$ codes $H(v)$, this
means that $H(n)$ asserts that $F(H(n))$, and we have the
desired fixed point.


Allow me to mention a few other things. First, it is
interesting to consider whether all fixed points of $F$ are
equivalent to each other. This is true after all when $F$
is tautological, for example, since any fixed point will
also be logically valid. Similarly, Goedel's "I am not
provable" statements are all equivalent to the assertion
that the theory is consistent, and this is how one can
prove the Second incompleteness theorem. But are fixed
points for a given $F$ always equivalent? The answer is no.
Fix any statements $A$ and $B$, and let $F(v)$ be the
statement, "if $v=[A]$, then $A$, otherwise $B$". Note that
$F([A])$ is equivalent to $A$ and $F([B])$ is equivalent to
$B$, so they are both fixed points.


Andreas raised the very interesting question in the
comments below whether the fixed point $A$ has $F([A])$
also as a fixed point. This is what we might expect from the infinitary example above. 
 The example of the previous paragraph shows, however, that
not every fixed point has this feature, since in that
example, $A$ is equivalent to $F([A])$, but $F([F([A])])$
is equivalent to $B$. But in this example, other fixed
points do have the feature. I am unsure in general about whether there must always be a fixed point $A$ such that
$F([A])$ is also a fixed point.


Lastly, I would like to mention that essentially the same
argument for the fixed point lemma has been used to prove
other fixed point theorems in logic. For example, the
[Recursion
Theorem](http://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem)
asserts that for any computable function $f$, acting on
programs, there is a program $e$ such that $e$ and $f(e)$
compute exactly the same function.


One can prove this in a very similar way to the fixed point
lemma. Namely, define H(v,x)={f({v}(v))}(x), where {e}(x)
means the output of program e on input x. Note that H is
running program v on itself, and then applying f, just as
the H in your argument. Now, let s be the function that on
input v, produces a program to compute H(v,x), so that
{s(v)}(x)=H(v,x). Let d be the program computing s, and let
e=s(d). Putting this together, we have


* {e}(x) = {s(d)}(x)= H(d,x) = {f({d}(d))}(x)
= {f(s(d))}(x) = {f(e)}(x).


So program e and f(e) compute the same function.


