2 added 571 characters in body
$F(A)$. ThusIf we could expect a strong version of this, thenwe would seek an $A$ has the property that it absorbsapplications of $F$, since $A$ is equivalent to $F(A)$.

In particular, $A$ is also equivalent F(A)$, and tocould continue, arriving at one solution attemptso on, taking$A$as expanding from the inside. Such aprocess leads naturally to the infinitary expression •$F(F(F(\cdots)))$. This works F(F(F(\cdots)))$
• Furthermore, this infinitary expression is itself a fixedpoint, in a naive formal way, since adding if $A$ is thatexpression, then applying one more $F$ doesn't changeresults in anexpression with the same formof the statement, which makes $A$ formally thesame as $F(A)$, exactly as desired. But of course itexpression doesn't count as a solution, of course, since it isn't weseek a well formedfinite well-formed expression, but it suggests an

What

Namely, what we need want to do instead is to capture in a single statement finiteexpression the idea self-expanding nature of that adding one more $F$ doesn't change$A$. infinitarysolution. The desired statement $A$ is should be equivalent toitself. Introducing So we introduce an auxiliary variable $v$ to represent the possibilities, we

(This last self-substitution part,about substituting v $v$ at v, $v$, is what allows oneon, capturing with just one substitutionin effect curling the self-expanding infinite tail ofthe infinitary fixed point effect mentioned above.)expression around onto itself.

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

Allow me to mention some a few other things. First, it is$B$, so they are both fixed points.

Andreas raised the very interesting question in thecomments 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, thatnot every fixed point has this feature, since in thatexample, $A$ is equivalent to $F([A])$, but $F([F([A])])$is equivalent to $B$. But in this example, other fixedpoints 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.

1

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.