"?>
← Gödel arithmetization applet |  Index  | Main project page | The Gödel number→

Gödel's fixed point theorem

This proof is based on Complete Proofs of Gödel's incompleteness theorems by B. Kim
This is the fourth step of my construction of a Gödel sentence. The third step is a way of converting a function in a programming language into an arithmetical formula. Although I haven't finished that step yet I thought it would be useful to skip to this one, firstly because it provides the most insight about Gödel's proof, and secondly it gives some useful pointers as to how the third step should be done.
If you want to find out more on how to get into this way of thinking you should read I am a strange loop by Douglas Hofstadter.
The thing is that, from step 1, we have a program which will convert between an arithmetical formula and an integer representing its coded form. Hence it is possible to think of any arithmetical formula which is written down just as a representation the corresponding integer and so we don't need to keep mentioning the conversion function. However, we need to keep in mind the following three things

1: An integer within an arithmetical formula

In the system given, it won't work if you expect the integer to represent itself in a formula. As mentioned in 1+1=2 we can represent 1 as 0' (encoded as 11) and 2 as 0'' (encoded as 91). For large integers it looks like we might need lots of dashes, but of course we have addition and multiplication, and so 0'''''''''''''''''''''''''''''''''''''''''' (i.e. 42), for instance, can be represented as 0''''''''''*0''''+0''. We can use a base other than 10 if so wished, and the function num(x) which does this conversion in step 3 uses base 3.
Some related reading
This book gives a clear explanation of the basics of the proof of Gödel's incompleteness theorem. It would be useful for those wishing to get a clear idea of Gödel's theorem without getting too technical, and to go further than what is given in most popular treatments of the subject
cover
My review of Godel's proof

Fixed, 1935
Artist: Wassily Kandinsky
I'm thinking in particular here of what would happen if we added ¬σφ as an axiom, which Gödel's theorem says can be done without creating inconsistency. The new axioms would have as a model a system of non-standard integers (also known as supernatural numbers). Then ¬σφ would be provable (its an axiom!), but then σφ would no longer be the undecidable sentence obtained by this procedure - this would be another statement σφ~. We wouldn't have a proof of ¬σφ~, but since this system is ω inconsistent, the argument in the above paragraph no longer works, so such a proof may well exist.

2:Deriving one statement from another

Suppose two statements are equivalent, that is they can each be derived from the other using the given rules of proof. Then clearly the numbers representing them aren't the same, but we have an equivalence class over the integers. We will write this as ↔. We may also talk in terms of one statement (i.e. integer) following from another.

2:An integer function

The outcome of step 3 is that if you have an integer function f(x) (implemented as a computer program) then it can be expressed as an arithmetical formula with one free variable. We will write such a formula as *f*. In particular you should note that
*f*(num(n))↔num(f(n)).

The Fixed point formula

Define the function diag(μ)=∃z (z=num(μ)∧μ)

Now for an arithmetical formula φ(x) with one free variable, we let
nφ=∃x (x=*diag*(z)∧φ(x))
and define σφ=diag(n)

Then σφ=∃z (z=num(n)∧∃x (x=*diag*(z)∧φ(x));)
↔∃x x=*diag*(num(nφ))∧φ(x))
↔ ∃x(x=num(diag(nφ))∧φ(x))
↔ φ(num(diag(nφ))) = φ(num(σφ))

What this is saying is that σφ is a fixed point of φ

The proof of Gödel's Theorem

From step 2 we have a function proof(x) which takes an encoded arithmetical proof, and returns the statement which it proves. Take φ(x) to be ¬∃y(x=*proof*(y)). Then
σφ↔¬∃y(num(σφ)=*proof*(y))
Suppose there existed a proof, represented by the integer k, of σφ. Then σφ=proof(k), from which it follows that num(σφ)=*proof*(k), and so∃y(num(σφ)=*proof*(y)) which is equivalent to ¬σφ, giving a contradiction. Hence there is no proof of σφ. But this is just what the statement ¬∃y(num(σφ)=*proof*(y)) (which is equivalent to σφ) is saying. Hence σφ is true, so it is impossible to prove ¬σφ. Thus neither σφ nor ¬σφ are provable from the given axioms

But wait a minute...

Maybe we were to quick to jump from there being no proof of σφ to the truth of ¬∃y(num(σφ)=*proof*(y)) and so the unprovabilty of ¬σφ. Certainly we know that there is no integer y which satisfies this. One has to be sure though that there might just be a proof of ∃y(num(σφ)=*proof*(y)), even if this isn't true for any given integer. This property is known as ω inconsistency. Now the standard model of the integers is ω consistent, and so we can't prove such a statement from the axioms given. However the more general version of Gödel's theorem says that any arithmetical system which includes the integers will have an undecidable statement. If we want to be able to prove this then we need to be able to deal with ω inconsistent systems. To do this we use look at the function proofsearch instead of proof. This function takes an integer (arithmetical statement) μ and searches through all integers to see whether they provide a proof of μ or of ¬μ. In the first case the function returns 1, in the second case it returns 0. Note that this function may not terminate, indeed what we are trying to prove is that sometimes it will not.

So, take φ'(x) to be *proofsearch*(x)=0
then σφ'↔*proofsearch*(num(σφ'))=0

Now suppose that there were a proof of σφ'. Then we could deduce that *proofsearch*(num(σφ'))=0, but we also have proofsearch(σφ')=1 which would imply 1=0, a contradiction. Alternatively, if there was a proof of ¬σφ' then proofsearch(σφ')=0 from which we can prove σφ' to be true, again a contradiction.
Thus neither σφ' nor ¬σφ' are provable the axioms - and this result can be extended to more general systems
Tachyos Home Page  |  Chronon Critical Points  |  Books I've read recently