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{[F]})$$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?
