Arithmetic fixed point theorem - MathOverflow

Arithmetic fixed point theorem

2010-07-07T11:28:35Z

I want to understand the idea of the proof of the artihmetic fixed point theorem. The theorem is crucial in the proof of Gödel's first Incompletness theorem.

First some notation: We work in $NT$, the usual number theory, it has implemented all primitve recursive functions. Every term or formula $F$ has a unique Gödel number $[F]$, which encodes $F$. If $n$ is a natural number, the corresponding term in $NT$ is denoted by $\underline{n}$. The function $num(n):=[\underline{n}]$ is primitive recursive. Also, there is a primitive recursive function $sub$ of two variables, such that $sub([F],[t])=[F_v(t)]$, where $v$ is a free variable of $F$ which is replaced by a term $t$.

Now the theorem assertions the following:

Let $F$ be a formula with only one free variable $v$. Then there is a sentence $A$ such that $NT$ proves $A \Leftrightarrow F_v(\underline{[A]})$.

This may be interpreted as a self-referential definition of $A$, which is, as I said, crucial in Gödel's work. I understand the proof, I just repeat it, but I don't get the idea behind it:

Let $H(v)=F_v(sub(v,num(v)))$ and $A = H_v(\underline{[H]})$. Then we have

$A \Leftrightarrow H_v(\underline{[H]})$ $\Leftrightarrow F_v(sub(v,num(v)))_v(\underline{[H]})$ $\Leftrightarrow F_v(sub_1(\underline{[H]},num(\underline{[H]})))$ $\Leftrightarrow F_v(sub_1(\underline{[H]},\underline{[\underline{[H]}]}))$ $\Leftrightarrow F_v(\underline{[H_v(\underline{[H]})]})$ $\Leftrightarrow F_v(\underline{[A]}), qed.$

But why did we choose $H$ and $A$ like above?

Answer by Carl Mummert for Arithmetic fixed point theorem

2010-07-07T12:36:32Z

In the end, the reason to choose things in that way is because it works, but in this case it's possible to explain what's going on.

For a warm-up, you can get some intuition for the method by looking at an easier English example of the same phenomenon:

", when preceded by itself in quotation marks, yields a true sentence.", when preceded by itself in quotation marks, yields a true sentence.

To explain the proof you gave, I will use $|n|$ to denote the formula that has Gödel number $n$. In the proof above, $H(n)$ should be read as asserting $F([|n|(n)])$, that is:

$H(n)$ says: $F$ holds of the number of the formula obtained by substituting $n$ into $|n|$

Thus $H([H])$ says,

$F$ holds of the number of the formula obtained by substituting $[H]$ into $|[H]|$

that is,

$F$ holds of the number of the formula obtained by substituting $[H]$ into $H$

So $H([H])$ asserts $F([H([H])])$.

(For informal clarity, I have intensionally not used underlines here.)

Addendum. It's impossible in general to construct a formula $J$ such that $J$ is literally the same formula as $F([J])$. Any typical Gödel numbering has the property that $n < [F(\underline n)]$ for every formula $F(x)$ and number $n$. But if $J = F([\underline J])$ then $[J] = [F(\underline {[J]})]$.

So, if our proof method is going to work with an arbitrary Gödel numbering, is has to be more indirect. The proof gives a formula $H$ so that $H([H])$ is provably equivalent to $F([H([H])])$, but not literally the same formula. This may help explain why proof proceeds the way it does.

Answer by falagar for Arithmetic fixed point theorem

2010-07-10T12:54:50Z

Another approach, I suppose, is to consider this as a kind of Cantor's diagonal argument. If you write a table with rows correspond to formula and columns correspond to integers then $sub([F],[t])=[F_v(t)]$ is just a formulae in $[F]$ row and $t$ column. Now, following Cantor's diagonal argument, you might want to consider diagonal of this table, which is $sub(v,num(v))$ and augment it somehow. Here is there $F$ comes in - you apply it to the diagonal and get $H(v)=F_v(sub(v,num(v)))$. Why should you? I don't know exactly. But it's similar to standard Cantor's argument.

Hence, $H(v)$ is a formulae with the following property: for every formulae $T(v)$ there exist $n$ such that $H(n) \Leftrightarrow F(T(n))$ (because of diagonal argument --- take row number $[T]$ and intersect it with diagonal). That's why we can take $n = [T]$.

Hence, if we take $T = H$, and $n = [T] = [H]$ we would get what we need.

Answer by Linda Brown Westrick for Arithmetic fixed point theorem

2010-07-11T08:17:54Z

Let's start out with the observation that there can be no formula $D$ with the property that for all $\varphi$, $$D([\varphi]) \iff \varphi([\varphi]).$$ For if such a $D$ existed, then defining the formula $E$ by $E(\underline{n}) = \neg D(\underline{n})$, we would have $$D([E]) \iff E([E]) \iff \neg D([E]),$$ a contradiction.

Now, the task is to show that given a formula $F$ of one variable, there is another formula $A$ such that $A\iff F([A])$. Well, if that's not true, then an improbable-looking thing would happen: for every sentence $A$, we would have $$\neg F([A])\iff A.$$

The reason this looks improbable is that the formula $\neg F$ looks fairly similar to the forbidden formula $D$ above. In fact, if I want to juice the similarity for all it's worth, I would explore what happens when $A$ is of the form $A = \varphi([\varphi])$ for some $\varphi$; then we would have $$\neg F([\varphi([\varphi])]) \iff \varphi([\varphi]).$$

But if this holds for all $\varphi$, we can define the forbidden $D$ by $D([\varphi]) = \neg F([\varphi([\varphi])])$. Contradiction.

Now out of this argument, let's extract the specific formula $A$ that we originally wanted. We are looking for an $A$ of the form $\varphi([\varphi])$. Our hint is to use the same formula $E([E])$ which destroyed our hopes about $D$ above. The context is new, but we define $E$ in the same way: $E([\varphi]) = \neg D([\varphi])$. That is $$E([\varphi]) = F([\varphi([\varphi])).$$

Now the only step that remains is the one you've already seen: checking that $A=E([E])$ in fact works.

Answer by Joel David Hamkins for Arithmetic fixed point theorem

2010-07-13T01:59:00Z

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.

Answer by David Corfield for Arithmetic fixed point theorem

2010-07-13T14:46:51Z

For a unified account which subsumes the First Incompleteness theorem, Russell's paradox and Cantor's theorem, try Yanofsky's paper A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points.

Answer by Peter Arndt for Arithmetic fixed point theorem

2010-09-22T15:17:47Z

A wonderful book about the general pattern is Smullyan's Diagonalization and Self-reference (but it also goes more specifically into arithmetic). I also just found this recent article which contains an exposition of Lawvere's diagonalisation argument, which makes sense in cartesian closed categories...

Smullyan's page 17, adapted to Lawvere's setting seems to give a very general formal description of diagonalisation.

Answer by Sridhar Ramesh for Arithmetic fixed point theorem

2011-05-28T03:25:34Z

You could have discovered the fixed point theorem yourself! You'd just need the problem to be motivated the right way. For example, let's look at it as a kind of programming challenge...

Suppose you wanted to write a program that referred to its own source code at some point.

You could try to write it in BASIC (or Java or Haskell or English or Peano Arithmetic or whatever your favorite programming language is). But, you might find that to be too tricky at first. So nevermind BASIC; you decide to instead simply invent a hypothetical new programming language BASIC++, which is just like BASIC, but augmented with built-in support for programs to be able to access their own source code: this language has a basic keyword "myOwnSourceCode" within it, which is to be interpreted as just what you'd think from the name.

How does one actually run a BASIC++ program? Well, one thing you might do with a BASIC++ program (let's call it P) is compile it into an ordinary BASIC program, by going through its source code and replacing every instance of the keyword "myOwnSourceCode" with, of course, the expression of the actual source code for P.

So now we know how to write BASIC++ programs which refer to their own source code (it's trivial by the design of the BASIC++ language), and we also know how to compile BASIC++ programs into ordinary BASIC programs.

Of course, by combining those two, this means you can write BASIC++ programs which refer to the compilation of their own source code into BASIC.

And then, by actually compiling such a program into BASIC, you're left with, in fact, an ordinary BASIC program which refers to (which is to say, does whatever the programmer wants it to do with) its own source code.

This is precisely the structure of the fixed point theorem: $F$ is some BASIC-definable function, the free variable $v$ (in a BASIC++ program) is the "myOwnSourceCode" keyword, $sub(P, num(P))$ compiles a BASIC++ program $P$ into ordinary BASIC, $H$ is the BASIC++ program which applies $F$ to the compilation of its own source code into BASIC, and $A$ is the compilation of $H$ into BASIC; thus, as an instance of the pattern above, $A$ is an ordinary BASIC program which applies $F$ to its own source code. [The fact that the free variable of $F$ was also chosen to be named $v$ in the presentation given in the question is, incidentally, an unnecessary and irrelevant distraction]

(Of course, in the arithmetic fixed point theorem, "BASIC" is instead "Peano Arithmetic", but it's the same fundamental construction, whatever the particular context it is to be interpreted in)

Answer by Gyorgy Sereny for Arithmetic fixed point theorem

2011-05-29T23:43:01Z

I think that the best way to capture the idea beyond the proof of the fixed point theorem is to mirror it in an ordinary language formulation and then translate it back to the first order language of arithmetic (cf. J.N. Findlay, Goedelian Sentences: A Non-numerical Approach}, Mind, Vol. 51, 1942, pp. 259-65.). Clearly, what we seek is a sentence asserting that it has a given property, that is, a sentence that says "I have the property p". But, in order for it to be formalizable, our sentence should consist of components with easily identifiable formal first-order counterparts. Therefore we cannot use such indexicals as `I'.
In order to circumvent the need for indexicals, we reformulate Grelling's paradox applying it to open sentences instead of adjectives:

(1) "x is heterological" is heterological,

where an open sentence is called autological if the property it attributes to x possessed by the sentence itself, otherwise it is called heterological. For example, "x consists of five words", "x is English", are autological, while "x is long", "x is German", are heterological. On the other hand, both in formal languages and in informal ones, the fact that an object has a property is expressed by a substitution of the name of the object into the open sentence expressing that property. Consequently,

(2) x is heterological just in case the sentence obtained by substituting the name of x for the variable in it is false.

Now (using the convention that he name of linguistic objects are the object itself between quotation marks), if we replace "being false" by "having property p", (1) and (2) together yield:

(3) the sentence obtained by substituting the name of "the sentence obtained by substituting the name of x for the variable in it has property p" for the variable in it has property p.

This is the sentence we need. On the one hand, it does not use indexicals, on the other, it indeed says of itself that it has property p (and says nothing else), since it is built up in such a way that if we perform the substitution described in it, then we obtain the sentence itself, which is stated to have property p.

Now, let s denote the open sentence between the quotation marks in (3), that is, let s be:

(4) the sentence obtained by substituting the name of x for the variable in it has property p.

Then, clearly, the whole sentence (3) is s("s"). In order to obtain the fix point lemma, we should translate it into the language of formal arithmetic. Clearly, the formalization process consists of two main steps. In the first step, we have to find the formal version $\eta$ of s, and then the second step is obvious: the desired sentence $\lambda$ will simply be $\eta(g(\eta))$ (where $g(\varphi)$ is the G\"odel number of $\varphi$ and plays, of course, the formal counterpart of name of $\varphi$, and, for simplicity, I leave out of consideration the difference between numbers and their formal counterparts in the language).

Now, that is all. That is the essence of the proof. What remains to do is simply translate the ordinary language argument into the formal language of arithmetic. That is a completely mechanical task.

Let us recall that what we should show is that, for any arithmetical formula $\varphi$ with at most one free variable (this fact will be denoted by $\varphi=\varphi(x)$), there is a sentence $\lambda$ such that

$Q\vdash \lambda \longleftrightarrow \varphi(g(\lambda)),$

where $Q$ is Robinson arithmetic (essentially Peano arithmetic without induction).

Now, let the formula corresponding to the property p be $\varphi=\varphi(x)$. Then, obviously, the formal version of s is $\varphi(g[x(g(x)])$. In order to continue the formalization process, we should find a formula that can play the role of $\varphi(g[x(g(x))])$, that is, a formula $\eta=\eta(x)$ such that $\eta(g(\psi))$ is provably equivalent to $\varphi(g[\psi(g(\psi))])$ for every $\psi=\psi(x)$, or equivalently (denoting the inverse of $g$ by $g^{-1}$), for any $n \in N$,

$Q\vdash \eta(n)\longleftrightarrow\varphi(g[g^{-1}(n)(n)]). $

In order to find the appropriate formula $\eta$, let us consider the expression substituted into the formula $\varphi$, and define the function $f:\omega\longrightarrow \omega$ accordingly:

$f(n)=g[g^{-1}(n)(n)]$ if $n \in N$ and $f(n)=0$ otherwise.

Since this function is obviously recursive and hence representable, and, up to provable equivalence, the result of substituting a representable function into a formula can also be expressed by a formula, there is a formula $\eta$ such that, for any $n\in N$,

(5) $Q\vdash\eta(n)\longleftrightarrow\varphi(f(n))$

Thus we have obtained what we need, we have shown that there exists an $\eta$ that can be considered to be the formal version of s. Now, all that remains to do is straightforward: it follows from (5) that, for every $\psi$,

$Q\vdash \eta(g(\psi))\longleftrightarrow \varphi\big(g[\psi(g(\psi))])$,

which, in turn, choosing $\psi$ to be $\eta$, yields

$Q\vdash \eta(g(\eta))\longleftrightarrow \varphi(g[\eta(g(\eta))])$,

showing that the sentence $\lambda =\eta(g(\eta))$ indeed has the desired property.