Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
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?
The incompleteness theorem is a jedi mind trick. All it proves is that monkeys can manipulate symbols that represent inconsistent formal systems. why don't you simplify that amazing proof: assert that true equals false, then sit around marvelling at the amazing paradox. ==
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:
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.
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.
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.
Upvoted even though "formalist delirium of the Hilbertians" is hardly helpful. Gödel's results did strike a blow against Hilbert's formalism, but it is hardly fair to characterize it as delirious; before Gödel's theorems (and possibly after) Hilbert's programme had a lot going for it as a position in the philosophy of mathematics.
@vanden Fair enough - I re-read and agree it sounded unecessarily pejorative; I didn't mean it like that - but to us, now, the Hilbertian goal must seem a tad delirious in its ambition. I added a bit on partial realizations of HP too. Personally I am not hostile to HP and do believe that Hilbert is grossly misrepresented when labelled a radical formalist because he in no way believed that (what he called) ideal mathematics was contentless - quite the opposite: he believed that the content of idealized mathematics is the same as that of elementary, intuitively graspable mathematics
It's a nice answer. You get +1 simply for "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."
From your answers about Gödel, I gather that you deeply appreciate his work on a technical level, but have a strong distaste for the ways it's often been applied.
@jaskey13: There is actually a close correspondance between Godels incompleteness theorem & the halting problem for Turing Machines. So Maimons interpretation is not entirely inappropriate.
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.
How is S and R related? Point 2 in the SPITE list is no too precise, I don't know why I'd know that the halting property of the program would be encoded or even encodable in the framework initiated by the S rules. I don't know how to translate the assumptions on S to a computer. What does the assumption imply or how is it justified. Proofs/strings are clearer to me than computation. Also, the line after "I assume S is consistent." is confusing to me. This has, I guess, something to do with what in Gödels original prove is formulated as an encoding of the prove in the language of arithmetic.
@NickKidman: I assume you know some universal computer, with memory M and instruction function f, so that the state after n clock cycles is f(f(f(..(f(M))...) (f iterated n-times on M). The main assumption on S is that: 1. it should prove for any fixed M that n-fold iterate of f on M is M' (where M' is the actual answer--- this is a finite calculation), 2. it should be able to form the sentence "(forall n) f-interated-n-times on M has not halted". These are both true in any reasonable model for mathematics.
The statement following "S is consistent" is just a reformulation of consistency. If S is consistent, and proves "P does not halt", then P cannot halt after n steps, because S knows what f-itereted-n-times on the initial memory state of program P is, and so it would prove that P halts, and this would be a contradiction. Conversely, if S is inconsistent, it will prove anything, including that a halting program doesn't. So S is consistent iff (S proves "P doesn't halt" implies P doesn't halt). On the other hand, S can prove "P halts" for nonhalting programs, this is an "omega-inconsistency".
Thank you for a immensely helpful essay. Much of it is over my head but this is my fault I utterly disagree with the argument you give to show machine consciousness is possible, an objection to do with the 'universal notion of computation' you mention. I would very much like to discuss this with you since I need to know if my objection holds. Do you have any time. eight years after posting your answer, to chat?
– user20253
CommentedNov 25, 2019 at 18:05
"Any two such machines are equivalent--- A can simulate B and B can simulate A." Is this technically true? Suppose A and B has m and n bits of memory respectively, and p bits is requires for the simulation program. For A to simulate B, it needs n + p bits of memory, so m > n. But for B to simulate A, we need n = m + p, but m > n so this is impossible. It is only possible for A to simulate B or B to simulate A, but not both.
The original question concerns the first incompleteness theorem, but some of the answers, including the highly upvoted answer https://philosophy.stackexchange.com/a/2645, delve into the second incompleteness theorem, and rightly so because a majority of the claimed philosophical implications are based on the second theorem.
Most of the philosophical implications drawn by both philosophers and laymen from Goedel's result have no basis whatsoever, because Goedel's theorem is incorrect in the following sense. A leading logician and computer scientist Artemov showed that the problem lies with Goedel's formalisation of the notion of consistency. A more realistic notion of consistency, closer to the notion originally envisioned by Hilbert, led Artemov to a proof of consistency of Peano Arithmetic within Peano Arithmetic. For details, see this answer. Therefore the informal claim that "a system at least as strong as PA cannot prove its own consistency" goes down the dustbin of history, along with myriad related commentaries and speculations.
Wow - This seems important. I took a very quick look at Prof. Artemov's MathOverflow post (not at the paper), and understand it's a question of exactly how to interpret the notion of "consistency" that is in play (or that is most "appropriate"?). I didn't directly understand the difference or why the new proposed definition is more appropriate (or closer to what Hilbert was asking for?) Are you able to make this difference a little more intuitive?
The question is specifically about the first incompleteness theorem, and your answer appears to be concerned with the second. Does a weaker version of the concept of consistency have the same consequence for the first theorem? Surely there are many ways to demonstrate that there are sentences within the language of PA that are neither provable nor disprovable within PA. So we don't even need Gödel's proof to know that the first theorem is correct.
@mudskipper, in a 0th approximation, Artemov's point is that consistency as envisioned by Goedel is too strong. Roughly , the difference is that the statements required for Goedel-consistency are labeled by all the object-theory integers, whereas the statements required for Hilbert-Artemov consistency are labeled by only the metalanguage integers that Artemov refers to as "numerals".
As far as I can judge from the various follow-up Q&As on MO, there seem to be some criticisms of his paper, namely that it uses steps that muddle the line between wff and meta-theoretical statements (on numerals?) and are not themselves provable in PA in order to reach the conclusion. I completely lack the education and skillset to judge any of that, though.
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.
What Gödel showed: In any mathematical system T that is strong enough, you can make a statement S which can in layman’s terms be interpreted as “in the mathematical system T there is no proof for the statement S”.
If S is true then it states there is no proof for S. So T is incomplete: There is a statement S that is true but has no proof.
Since S states there is no proof for S, if S is false then there is a proof. So there is a statement S that is false but has a proof, meaning T is contradictory.
Together, T is either incomplete or contradictory. Being incomplete would be bad news. Being contradictory would be much worse, it would mean the mathematical system T has no foundation whatsoever and would be complete nonsense.
We therefore call it “Gödels incompleteness theorem, because incompleteness is something we can live with.
Etended quete: "A second analogy becomes apparent when we reformulate the main result in still another way. Recall that an observable is called infor-mationally complete if by measuring it one can distinguish all the states. Now the main result can be formulated in a way reminiscent of Goedel’s incompleteness theorem: No measurement from inside the observed system can be informationally complete. These conclusions are valid for classical systems as well as for quantum systems, and irrespective of the character of the time evolution."
"If a theory is universally valid in the absolute sense, it does not allow for an observer not described by the theory. Take Ou to be the biggest system described by an absolutely universally valid theory. (Ou might be called the “world”, or the “universe”.) As all potential observers are described by the theory, Ou does not have any outside observer. If, and this is a slightly stronger assumption, the union of all observers fulfils the assumption of proper inclusion, then by Theorem 1 there are some states of Ou which cannot be measured exactly by any observer, not even by all of them together
Hi @Anixx. Can you please put your comments into the answer (they give a good description of the link). In general, link only answers with only a sentence of explanation are discouraged (Such really is a comment).