Godel's theorem
I would like to pause here to first precisely state and prove the Godel theorem properly. The original presentation is before the invention of the computer, and is complicated. But we live 80 years later, where computers are familiar.
First, in Godel's theorem, you are always talking about an axiomatic system S. This is a logical system in which you can prove theorems by a computer program, you should think of Peano Arithmetic, or ZFC, or any other first order theory with a computable axiom schema (axioms that can be listed by a fixed computer program).
Such an axiom system is assumed to be able to describe a computer at any finite time. The memory contents of a computer is a string of bits, a large integer M, and the manipulations on the memory from running one step is a very simple function, which does something from the instruction set and changes the memory. If you do this a finite number of times, you get a new memory state M'. The basic assumption on S is this:
S can follow a computer program: given a fixed universal computer with initial memory M, it will prove that the memory at time t is M' for any finite time t.
In Peano Arithmetic this is trivial, because you can code a computer's memory in very simple ways, and the axioms without induction, just the axioms for calculating stuff, tell you what the result of a finite calculation is. So this is true in Peano Arithmetic without induction and without quantifiers. It's a very simple thing to ask of an axiom system--- that it can follow a computation and prove that the result at finite time is correct.
Next, we assume that S can state things like "Program P does not halt". This requires a quantifier
I assume S is consistent. The statement "S is consistent" means that if S proves "P does not halt", then P in fact does not halt. Since if P halts, S would follow it until it halts, and then prove this too. Note that S can prove "P halts" without P actually halting, it just can't prove "P doesn't halt" if this is a lie.
Theorem: Consider such an axiom system S. There is a program P which doesn't halt for which S can't prove "P doesn't halt":
Proof: Write the computer program SPITE to do the following:
- Print its own code into a variable R
- Deduce all consequences of the axioms of S, looking for the theorem "R does not halt"
- If it finds this theorem, it halts.
If you think about it for half a second, the moment S proves "SPITE doesn't halt" SPITE halts (by construction) and makes S a liar. The self-reference is in the first line--- printing your own code into a variable, and that this is possible is an exercise given to undergraduate programmers.
That's the complete construction, and the complete proof.
Godel 2: S cannot prove itself consistent
The proof is as follows: if S is consistent, SPITE can't halt, because we see that this implies S is inconsistent. So if S can formalize this argument and it can prove itself consistent, it proves SPITE does not halt (which is impossible).
That's the complete proof. It requires familiarity with logic to see that for appropriate S, the informal deduction "S is consistent implies SPITE doesn't halt" can be formalized in S, but if it weren't possible to formalize intuitive logical deductions like this, we wouldn't be using S in the first place.
Rosser: The problem with Godel1 and Godel2 (which are essentially the same theorem up to a trivial choice of canonical example), is that S could still be complete but wrong. In other words, Godel's proof didn't show that there is a program P whose halting is not predicted at all. Maybe S decides all programs either halt or don't halt, but it doesn't get it right--- it tells you that some non-halting programs halt. If it told you that a halting program didn't halt, this would be a contradiction in S (after enough time), but it can tell you a non-halting program halts without contradiction (this is obvious, but subtle).
So write ROSSER:
- Prints its code into R
- Deduces from S, looks for a) "R prints to the screen" b) "R doesn't print to the screen".
- If it finds a) it halts without printing. If it finds b) it prints "hello" and halts.
Now S cannot prove either "ROSSER prints" or the negation "ROSSER doesn't print". So that if a second program follows Rosser and halts when ROSSER prints, this program is not proved either halting or non-halting.
Philosophical implications
The main philosophical implication is the most important in the history of philosophy (this is not an overstatement):
There exists a universal notion of computation, which is independent of the axiom system.
This is the main result of Godel's work, although it wasn't fully understood until Turing's version a few years later. But Godel was groping towards this, as he understood this was true very quickly after proving the theorem, and he recognized Turing as having provided the explanation and abandoned his own approach to computation in favor of Turing's. The reason I can get away with such a proof as above is because we all are familiar with the notion of "a computer" and "a computer program", and we all know that any precise algorithm can be programmed on a computer, and that one computer is as good as another.
Immediate philosophical implications:
There is an agreed-upon notion of what it means to have a precisely defined set of rules.
You can actually build a machine which can simulate any other precisely defined set of rules.
Any two such machines are equivalent--- A can simulate B and B can simulate A.
If physics exists (if there is a precise set of rules, even probabilistic rules, to model nature), the universal machine (equipped with a random number generator) can simulate anything in nature.
From this it follows that:
The complete behavior of the human being can be simulated by a universal computer.
With the plausible logical positivistic assumption, this means that
A computer is a machine capable of thinking.
This insight is due to Turing. Von Neumann has the following insight:
A computer is a machine which is capable of modelling the behavior of biological systems. Godel's theorem is analogous to self-replication.
These are far and away the most important philosophical insights of all time. The precurser to this is Liebnitz attempts to make a philosophical machine, which could reason mechanically. Leibnitz understood a few of the implications of a computer.
Philosophical implications of Godel's theorem itself
Godel's theorem showed that, if you take the philosophical position that the statement "program P doesn't halt" is absolutely meaningful, then there is no fixed axiomatic system capable of proving all these meaningful truths. This is sort of obvious--- the program deducing from the axioms can't prove too much about itself without contradiction.
But more importantly, it shows you how to produce stronger systems--- by adjoining the axiom "S is consistent", you get a new system which makes the system stronger. This means that any axiom system has a stronger one, the Godel reflection
S + "S is consistent"
is strictly stronger than S.
You can iterate this procedure, by iterating the Godel reflection. There is no barrier at infinity--- you can consider the system which is the infinitieth Godel reflection to be the union of all the theorems proved at the n-th stage (there is a specific program which will print out the deductions--- you don't need set theory to make the iteration precise, at least not for small enough infinite ordinals). The process of iterating Godel's reflection reproduces Cantor's ordinals.
This answers the question of mathematical philosophy
Why are ordinals necessary?
It completely justifies Cantor's set theory. Cantor's set theory is required to give Godel reflections of theories past omega. It doesn't justify all the metaphysics, however, just the ordinals past the integers.
As you go up the ordinal list, the ordinals are ever more complicated computer programs (each ordinal is a "process" in Paul Cohen's words). Traditionally, you can define the limit of all ordinals that can be represented on a computer within a set theory, and this is called the Chuch-Kleene ordinal. You can only approach the Church-Kleene ordinal in complexity.
Further development
After Godel, Gentzen proved the consistency of Peano Arithmetic within a very limited axiomatic system (PRA--- a weak fragment of PA) with the additional assumption
The ordinal epsilon-naught is well founded
From this point on, it was clear that consistency proofs of complicated theories can be given from simple theories with the only complex assumption the well-foundedness of a certain countable computable ordinal. For PA, the ordinal wasn't even all that complicated, so that there are questions (like the Paris-Harrington problem, or the hydra problem, or Goodstein's theorem) that are equivalent to the well-foudedness of epsilon-naught, and so cannot be proved within PA, but which are equivalent to the consistency of PA, so they are provable in any theory that can prove the consistency of PA.
The subject of ordinal proof theory attempts to match an ordinal, as explicitly describable as possible, to each mathematical theory. This program has has success with certain set theories, and there is no barrier for it proving the consistency of any theory, no matter how infinite. So another implication is
It is possible to complete Hilbert's program, and prove the consistency of uncountably infinite mathematical systems, only using countable computable ordinals which can be represented on a computer.
This program is active today, but it has still not proved the consistency of ZF. Partly this is because many people continue to say that this cannot be done, because of Godel's theorem.
The main assumption in these ideas is that the process of producing ordinals which approach the Church Kleene ordinal can be somehow understood, although it is not formalizable as a computer program. This process is a gain in complexity analogous to biological evolution, and how far we can go within our human limitations is not understood.
False implications
There are many false implications of Godel's theorem
We are more than computers
This interpretation comes from the fact that we can understand that a program P doesn't halt (namely SPITE for a given formal system) even though the formal system can't. To see that this is a false conclusion, you just have to look at what SPITE does: it simulates the system, looks for the prediction, and spites it! There is no reason you can't do that to a person:
If you can simulate a person, you can predict their choice, and spite their decision--- so that you can place a million dollars in box A only if the person will choose box B.
This is the exact analog of Godel's theorem in the human realm, and it is a famous philosophical problem. There are also statements
John Searle cannot consistently believe this statement
that are exactly analogous, and that John Searle cannot believe, although it is true. Although to make it a first-order logic statement about arithmetic, you have to give a computational model of Searle's beliefs, which might not be possible due to the randomness. But the idea is the same--- the things the axiom system cannot know, but we can know, are things about the system itself.
There are further constructions due to Chaitin, which rephrase the incompleteness theorem as follows
No program can prove that any string has Kolmogorov complexity greater than the length of the program plus a fixed constant
But in a computational view of people, this just means that no human can prove that a string has Kolmogorov complexity greater than the complexity of a program which simulates this human. Since we have such a hard time even with small Kolmogorov complexity, this is a safe prediction.
So there are no consequences of Godel's theorem that imply that the computational theory of mind is false. There are other ideas
Godel's theorem says semantics isn't formalizable
This is not exactly true either--- Godel's theorem says that the semantics of halting computer programs is only approximately axiomatizable by strengthening systems, and the process of strengthening is non-algorithmic at the high end. But the precise nature of the non-algorithmicness might be a simple as naming ever larger computable countable ordinals that approach the Church Kleene ordinal, and this might be evolutionarily possible in a reasonable way.
Gode's theorem kills Hilbert's program
inasmuch as Hilbert's program developed ordinal analysis in response to Godel's theorem, this is not true. It does make a naive implementation of Hilbert's program impossible, but the ordinal analysis view is not at all naive, and is precisely the kind of foundations one can expect for mathematics which is infinitely rich and infinitely complex.
