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 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.