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)$. Thus, $A$ has the property that it absorbs applications of $F$, since $A$ is equivalent to $F(A)$.
In particular, $A$ is also equivalent to $F(F(A))$, and we could continue, arriving at one solution attempt, taking $A$ as the infinitary expression $F(F(F(\cdots)))$. This works in a naive formal way, since adding one more $F$ doesn't change the form of the statement, which makes $A$ formally the same as $F(A)$, exactly as desired. But of course it doesn't count as a solution, since it isn't a well formed finite expression.
What we need to do instead is to capture in a single statement the idea that adding one more $F$ doesn't change $A$. The statement $A$ is equivalent to the assertion that $F$ holds when substituted at $A$ itself. Introducing an auxiliary variable $v$ to represent the possibilities, we 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 part, about substituting v at v, is what allows one substitution to self-expand into two, and then three and so on, capturing with just one substitution the infinitary fixed point effect mentioned above.)
Namely, if $n$ is the code of $H(v)$, then we perform the one 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. We could have kept expanding to $F(F(H(n)))$, but we've already caught our tail.
So that's it. But let me mention some 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.
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.