What are the philosophical implications of Gödel's First Incompleteness Theorem?

Question

Gödel's First Incompleteness Theorem states

Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250).

What are the philosophical implications of this theorem? In particular, are there possibly more general analogues of this theorem -- necessarily "unprovable truths" within other kinds of formal systems?

Answer 1

Any effectively axiomatized formal system that extends a very basic theory of formal arithmetic called Robinson Arithmetic (Q) will contain an undecidable sentence. In full generality, you can state the syntactic version of the First Incompleteness Theorem as follows:

(G1T) For any effectively axiomatized theory T that extends Q there exists a T-sentence G such that: (i) If T is consistent then T cannot prove G (ii) If T is omega-consistent then T cannot prove ¬G.

This is as general a statement of the theorem as you can get. Note that Kleene - in your quotation - is talking about the semantic version of the theorem. What Godel originally proved however involved no semantic notions such as truth, arithmetical truth etc. Whether or not you can see/recognize/acknowledge G as true depends on the semantic/intensional understanding of G - it is a common misconception that Godel wanted to prove the limitations of arithmetical truth. The background he was working against was Hilbertian formalism - so his primary concern was to demonstrate the purely syntactic limitations of formal systems. So, in full syntactic generality, (G1T) says (informally) that no approriate manipulation of symbols in any formal system complicated enough to contain some arithmetic will end up with G.

So you can see that (G1T) applies to a vast array of formal systems. Whether you choose to see the G's obtained as 'unprovable truths' depends on your semantics/ on whether your T has an intended interpretation and so on. But in most usual cases that kind of conclusion is considered justified. But it only arises because of the subvenient syntactic glitch that (G1T) ensures.

Now as for philosophical implications, the literature is immense. I will mention some pertinent issues:

1. Some people have seen (semantic) (G1T) as a cogent argument against mechanism, i.e. against the thesis that minds are machines. The locus classicus is Lucas' Minds, Machines and Godel. Penrose extends and fortifies the argument in his books on consciousness. Ripostes to these arguments abound, see especially Putnam's Minds and Machines.
2. Michael Dummett in the aptly titled 'The Philosophical Significance of Godel's Theorem' has argued that (G1T) may be construed as an argument against the thesis that meaning is use, by demonstrating to us that the use of any symbolic manipulation is always outrun by arithmetical truth and meaning. He introduces the notion of indefinite extensibility to salvage the thesis and provokes a lot of debate along thhe way.
3. There are certain versions of Hilbert's Programme (HP) that can be said to have been refuted by (G1T). Nevertheless it is usually the Second Incompleteness Theorem that most people take to be the final nail in the coffin of (HP). Arguably this is the most monumental philosophical contribution of Godel's epoch-making discovery, namely that it single-handedly refuted Hilbertian formalism. Although, again, there are some research projects that can be seen as partial realizations of HP that are being carried out to this day - especially noteworthy in this direction are Detlefsen and Feferman.

Finally, I should like to say that countless philosophically-minded authors/thinkers/hacks have appropriated Godel's Theorem to try and make points about self-reference/loops/God/metaphysics/environmental awareness and God knows what else. The three implications I raised may seem dry and academic but they are also precise, well-studied and free from hyperbole. There is no doubt that Godel's theorems propelled our understanding of formal systems forward - and with it, our understanding of the philosophical powers and weaknesses of formal reasoning.

Answer 2

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:

1. Print its own code into a variable R
2. Deduce all consequences of the axioms of S, looking for the theorem "R does not halt"
3. 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:

1. Prints its code into R
2. Deduces from S, looks for a) "R prints to the screen" b) "R doesn't print to the screen".
3. 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.

Answer 3

I think there are also some consequences for the philosophy of mathematics, in particular for the radical formalist view which considers mathematics as a mere formal game without any actual meaning. This view has a problem with Godel's result: the theorem indeed shows that we are able to make mathematical inferences outside any possible fixed (and strong enough) formal setting, so if math is just "playing with formal rules" it's not clear how to identify these rules in any reasonable way since any possible set of rules you can provide happens to be unreasonably weak by Godel's result.

Answer 4

No measurement from inside the observed system can be informationally complete.

https://homepages.fhv.at/tb/cms/?download=tbDISS.pdf