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
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.
Raymond Smullyan gave a very general formulation in terms of representation systems. They appear in his "Theory of Formal Systems", and in the first and last chapters of "Godel's Incompleteness Theorems". They generalise first- and higher-order systems of logic, type theories, and Post production systems.
A representation system consists of:
A countably infinite set $E$ of expressions.
A subset $S \subseteq E$, the set of sentences.
A subset $T \subseteq S$, the set of provable sentences.
A subset $R \subseteq S$, the set of refutable sentences.
A subset $P \subseteq E$, the set of (unary) predicates.
A function $\Phi : E \times \mathbb{N} \rightarrow E$ such that, whenever $H$ is a predicate, then $\Phi(H,n)$ is a sentence.
The system is complete iff every sentence is either provable or refutable. It is inconsistent iff some sentence is both provable and refutable.
We say a predicate $H$ represents the set $A \subseteq \mathbb{N}$ iff $A = \{ n : \Phi(H,n) \in T \}$.
Let $g$ be a bijection from $E$ to $\mathbb{N}$. We call $g(X)$ the Godel number of $X$.
We write $E_n$ for the expression with Godel number $n$.
Let $\overline{A} = \mathbb{N} \setminus A$ and $Q^* = \{ n : \Phi(E_n,n) \in Q \}$.
We have:
(Generalised Tarski Theorem) The set $\overline{T^*}$ is not representable.
(Generalised Godel Theorem) If $R^*$ is representable, then the system is either inconsistent or incomplete.
(Generalised Rosser Theorem) If some superset of $R^* $ disjoint from $T^*$ is representable, then the system is incomplete.
In case it's not clear: in a first-order system, we can take $P$ to be the set of formulas whose only free variable is $x_1$, and $\Phi(H,n) = [\overline{n}/x_1]H$.
Best Answer
Presburger arithmetic does NOT prove its own consistency. Its only function symbols are addition and successor, which are not sufficient to represent Godel encodings of propositions.
However, consistent self-verifying axiom systems do exist -- see the work of Dan Willard ("Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles"). The basic idea is to include enough arithmetic to make Godel codings work, but not enough to make the incompleteness theorem go through. In particular, you remove the addition and multiplication function symbols, and replace them with subtraction and division. This is enough to permit representing the theory arithmetically, but the totality of multiplication (which is essential for the proof of the incompleteness theorem) is not provable, which lets you consistently add a reflection principle to the logic.