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

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.

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

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.