Goedels Incompleteness Theorem

Descriptions of the theorem have been merged in from GoedelsTheorem.

Discussion of the implications and consequences of the theorem have been extracted to GoedelsIncompletenessConsequences.

-- AndrewMcGuinness

Goedel's First Incompleteness Theorem: Any adequate axiomatizable theory is incomplete. In particular the sentence "This sentence is not provable" is true but not provable in the theory.
Goedel's Second Incompleteness Theorem: In any consistent axiomatizable theory (axiomatizable means the axioms can be computably generated) which can encode sequences of numbers (and thus the syntactic notions of "formula", "sentence", "proof") the consistency of the system is not provable in the system.

Imagine you do mathematics. Any kind of mathematics will do, for example number theory. Imagine further you have finally figured out what a proof is, and formalized it in a reasonable way. Let's call this a formal proof.

Now, if your number theory is powerful enough, you can formulate the following statement (in number theory):

: This statement has no formal proof.

Now, if that statement is false, then it has a formal proof, and unless your proofs are really weird this means that the statement is true anyhow.

On the other hand, if the statement is true, then there is no formal proof. Thus, you have a statement which is true, but with no formal proof.

This is independent of your initial idea of what a proof was. Thus, whenever you figure out what a proof is we find a statement which has no proof, even though it's true. Weird, isn't it?

The above is a typical Platonistic mischaracterization of what Goedel actually managed to prove. In what way is the sentence "this sentence is not provable" true if it is not provable? It is only true OUTSIDE of the theory in question. It is only true in the natural-language general-reasoning system which we happen to possess. And it would be false in a different but just as viable general reasoning system which we happen to not possess. The fact that a theory is consistent with EITHER its Goedel sentence OR its negation has been known for a long time.

[[Uh, no. Unless Gödel's proof and other similar ones are flawed (after 70 years of examination of a fairly simple proof, mathematically speaking) or Peano Arithemetic is so flawed as to be inconsistent (and who thinks that?), then its result is just plain and simple true, not "only true OUTSIDE of the theory in question". Although the sentence does not quite say "this sentence is not provable", but rather "this sentence is not provable in this system".]]

The fact that our minds happen to possess one system (one in which "this sentence is unprovable seems obviously true") and not the other (in which it would seem obviously false) is not a proof of truth. It's a proof of exactly nothing.

A proof of "exactly nothing" ironically could be a proof of anything, if nothing is anything (i.e. something from nothing, Krauss). Furthermore, "exactly nothing" might be a paradox. What is "exactly nothing"... if nothing doesn't exist it can't be "exact".

So in fact, the sentence "this sentence is not provable", being unprovable within the theory, is neither true nor false in that theory, and is either true or false depending on which more powerful theory you choose to use.

As a working mathematician, this sounds like nonsense. You ask: "In what way is the sentence "this sentence is not provable" true if it is not provable?"
- It is true in the sense that if it is false then the system is not consistent. The system has been assumed to be consistent, therefore it cannot be false. Thus it must be true.
  - One then wonders. If the falsity of the statement would make the system inconsistent, would that not constitute a proof (of the statement) by contradiction?
- Clearly if you reject a bi-valent system then there is a whole new can of worms, but what you have said here simply doesn't make sense to me. Perhaps you could express your ideas more formally to ensure that there are no gaps in your reasoning.

[[This faulty reasoning is an artefact of the misrepresentation at the top of this page. Goedel actually showed that a construction that amounts to "No number is the encoding of a proof for this sentence." can neither be proved nor disproved, for if either was the case, the system would be inconsistent.

Now is this sentence actually true? Can't be said. It can be made true (there is no such proof, therefore no such proof number) or it can be made false (there is such a proof and it has a "surreal" number). Both extensions of the axiomatic system are consistent, both give rise to a new system with at least one new "Goedel sentence", and so on.

The wrong introduction on this page really should be corrected and the rest be refactored accordingly.]]

I didn't write that, but it's somewhat similar to things I have said. I personally would say that this does motivate new searches for modifying the law of the excluded middle, although no one has found a really generally useful way to do so thus far, so yes, it's a can of worms. This is related to the ongoing research looking for new systems of logical inference in general.

Also, just as a btw, I have been slowly getting the impression that working mathematicians in general all feel they understand Goedel's results, and yet some seem to have contradictory understandings. I need to keep more careful notes in the future to prove that this occurs, so maybe not - but I really think so (present company excluded, of course).

I distinguish carefully between assigning "truth values" to logical propositions, and any external concept of "truth". The latter stirs muck from the bottom of settling pools. Talking of "truth values" and avoiding the notion of Truth does very well. When anyone strays from such formal statements and starts to talk about applicability of Goedel's theorem to anything else, they are no longer doing mathematics. Then whether they are a working mathematician or not, they're playing a different game.
In this context, Goedel's Theorem takes a heap of well-formed strings and assigns some of them the colour blue. Then there are rules for taking coloured strings and using them to deduce the colours of other strings. Goedel's theorem states that if your rules are "interesting" in some formal sense, there are strings whose colours cannot be deduced. Further, it shows that we can deduce there is at least one string such that if it were coloured red then we would then be able to use the rules to colour some other string both red and blue.
Does that formulation remove some of the problems?

It should, except I assumed such things already, and assumed you assumed such, also. :-) Note that I disagree with the other author's claim that "It's a proof of exactly nothing". On the other hand I think it is slippery as to what is and is not proven. For instance, elsewhere on this page there is some discussion of finiteness of axioms, but sadly without noting the issue of infinite "axiom schemes". The use of such does not infinitely increase the power of the system because the scheme is still generated from a finite amount of information (the symbols used to describe the infinite axiom scheme tower), whereas to reach the next level in power, one would need an actual infinite amount of axiomatic information, which humans can never provide. This is transformationally equivalent to the unreachability of almost all transcendental numbers.

In neither case is the issue trivial; it's important to know that e.g. although we can sometimes add useful notations such as Lambert's W function, we will never have enough elementary functions to express everything in closed form (which is again transformationally equivalent). On the other hand, this does not prevent us from doing indirect non-closed form analysis on many things. Similarly with what Goedel does and does not allow. Similarly with what Turing does and does not allow; one can sometimes reason indirectly about the behavior in the limit of Turing machines that do not halt (or informally, that halt after an infinite number of steps).

I.e. too often interesting results like Goedel and Turing are interpreted to mean that almost everything is impossible, whereas actually, it's more along the lines of saying that certain methods almost always fail. Big difference. Further, measure zero isn't equal to zero, yet that's a common confusion, and again, it makes a big difference. We can prove whether some Turing machines halt, and that's often useful.

I should add that this is very much like the way that it took a long time for people to become comfortable working in the ring of formal power series, where the usual issue of convergence is a non-issue. This is a formal equivalence, in fact, since one can map between the space of Turing machines and that of power series, with equivalent norms related to halting and convergence, respectively.

Named for KurtGoedel, who put forward this theorem and proved it in the 30's, thus bringing the 'Hilbert Programme' crashing down about its ears. Much abused in later years as a touchstone phrase by the pseudo-philosophical for explaining anything (see also HeisenbergUncertaintyPrinciple, SocialDarwinism, ChurchTuringThesis, SapirWhorfHypothesis).

In 1979, DouglasHofstadter wrote a Pulitzer-prize winning book, GoedelEscherBach, an Eternal Golden Braid which gives a much better and quite accessible description of the theory, and makes connections between it and many other things. A classic, though not a light read.

(As an aside: When there's no "ö" available, a German would typically use "oe" instead -> "Gödel" becomes "Goedel". Same with ä and ae, and ü and ue, as in -- FalkBruegmann/FalkBrügmann)

What is the Name of this Book? and most of the other puzzle books by RaymondSmullyan lead to coverage of the Incompleteness Theorems by the end of the book.

A quick summary:

He wrote the theorem to disprove the workability of formal mathematical systems which attempt to provide a framework through which every mathematical question could be defined and proven without inconsistency and paradox. Once again you have a method where a natural number codes for a sequence of symbols, which this time are the mathematical definition of a particular function (in this case, we'll use a one-parameter function):

  : Fn(w)

Naturally there is a proof to the nth function (as is the point of creating formal mathematics):

: Pn

Now consider the following function (written out in English):

  : There does not exist x such that Px proves Fw(w).

  : (symbolically for easier reference: ~Ex[Px proves Fw(w)], where ~ = not,
 E = there exists, [...] = such that ...)

As Fw() acts upon w itself and x is defined within the system, this is a one-variable function with a boolean result. We'll consider our proposed function the kth function:

  : Fk(w) = ~Ex[Px proves Fw(w)]

Say we equated w to k:

  : Fk(k) = ~Ex[Px proves Fk(k)]

Which when written out:

  : There does not exist x such that Px proves Fk(k).

Which means that there is no proof for this perfectly well defined function Fk(k). This would mean that Fk(k) is false as an arithmetical proposition. Wait a minute . . . our system just proved a false proposition correct! This means there is in fact NO proof to Fk(k). We know that Fk(k) is true but the system has no way of coming up with that response on its own.

In other words, through mathematical INSIGHT we've determined a mathematical proposition, which means that there is some other mechanism(s) than algorithms that allow us to perform mathematical operations, which means that our minds are not algorithmic in nature!

The above stolen from my OAC Computers seminar on ArtificialIntelligence and ArtificialLife; most of that can be sourced to RogerPenrose's TheEmperorsNewMind. -- SunirShah

Another Quick Summary:

Roughly: "Any formal system that is free of contradiction and capable of proving enough statements about mathematics has undecidable propositions (i.e., sentences that it can neither prove nor refute)". Often abused by philosophers. [Pseudo-philosophers definitely, actual philosophers? I doubt it.] [J R Lucas is, I believe, an "actual philosopher", and he certainly abused Goedel's theorem.]

More precisely: A formal system of logic typically tries to divide propositions into a set of equivalence classes, usually labeled TRUE and FALSE. There are those sentences which can be so classified. Those sentences form the (usually infinite) set of "decidable" sentences. If we assume the consistency (being free of contradiction) of the formal system, there exist those sentences which are not decidable, and the (often missed) point is that you can't always tell which is which.

Goedel's construction yields a proposition that is not only undecidable - it is trivially True (not TRUE as in a formal system, but True among thinking humans). So, if we allow ourselves the use of the undefined 'True', we can restate his theorem in sharper (and more disquieting) form: "Any formal system that is free of contradiction and capable of proving enough statements about mathematics has undecidable propositions that are True."

For an opposing view (together with discussion pro and contra) on the truth of Fk(k), see IsFkkActuallyTrue. Also see PenroseCannotConsistentlyAssert.

An aside - in http://psyche.cs.monash.edu.au/v2/psyche-2-07-feferman.html (a commentary on ShadowsOfTheMind) Feferman states that the Hilbert program does work - in reverse! (i.e., mathematics as we use it can be made consistent, but top-down, not bottom-up. See para 4.5 of Feferman's article) I may have misunderstood this - can StephanHouben or any other lurking mathematicians comment?

I'm not sure whether you've misunderstood it, but I wouldn't express it in the terms you used. What Feferman says is that we can sometimes prove that one system is consistent provided another system is, and that often the "another system" is a lot weaker (hence, more obviously consistent) than the first one. In particular, you can get enough for practical purposes (literally "for practical purposes": Feferman says "all of scientifically applicable mathematics") without assuming anything more than the consistency of "Peano arithmetic"; that is, the elementary properties of the natural numbers.

: That's good to know, but it doesn't quite count as having the Hilbert program "work in reverse". Hilbert was after a proof that mathematics is consistent, not a proof that mathematics is consistent provided some of mathematics is consistent.
: I'd also quibble over the term "made consistent"; clearly it's not in our power to make mathematics consistent. But I don't think you really meant to imply that it was...
: -- GarethMcCaughan (lurking mathematician)

Roughly, the properties a system needs to have are (1) enough "regularity" that, e.g., a computer could list all its theorems (if given infinite time), and (2) enough "power" to talk about certain parts of mathematics. #2 needs a little more explanation: what's required is that all primitive recursive relations should be "definable" in the theory. I can give more details if you want, but we're in danger of getting (in your words) "very technical" here...

The "problem domain" is "whatever can be expressed in the language of the system". It's actually cleaner to state Goedel's theorem in a way that doesn't talk about systems "answering questions" or whatever; what it says is that in any system with the required characteristics, there are statements in the system's formal language which cannot be proved or refuted using the axioms and inference rules of the system. (If you're still left asking what the problem domain is, that's just too bad. It was you who introduced the term "problem domain" to the discussion. I don't think it's helpful here.) -- GarethMcCaughan

I also understand the problem domain to mean the set of statements expressible in the formal language of the system. However, I think it is helpful to give it attention since people too frequently believe the problem domain to be English sentences, or they don't draw any distinction between the axiomatic set and the formal language, or they crow in delight that you run into trouble if you allow the axiomatic set and the formal language to reference each other; as if that wasn't entirely predictable! -- rk

It's only "entirely predictable" because Goedel's theorem and Russell's paradox and a whole bunch of other instances of self-reference causing trouble have entered the general consciousness (that of the mathematically-inclined, at least). I'm not actually sure what you mean by "run into trouble" here, anyway.

I have no problem thinking that my beliefs are obvious only from my cultural perspective but since we're talking about people who do share my cultural perspective (laypeople and mathematicians now and not a century ago), I don't see what's the big deal.

It seems that by "predictable" you mean "predictable, if you're told the answer in advance". This seems a suboptimal way of using the word, to me. -- gjm

I'm sorry but I don't believe that "This sentence is false." is some kind of modern invention, let alone the earth-shattering statement most people believe it to be. When you allow mutual reference, caca happens. The lesson I take from it is to prohibit mutual reference.

That was a primary goal of Principia Mathematica, and is precisely what Goedel's Incompleteness Theorem proves cannot be done. His accomplishment was not in creating the CretanParadox - as the name implies, the key paradox is ancient - but in demonstrating that it is intrinsic to formal logic. Goedel demonstrated that any system of formal logic either is subject to his encoding scheme, and thus inconsistent, or else cannot express all true statements of mathematical logic. In any complete system, circularity cannot be prevented. -- JayOsako

There is no reason why an intelligent, rational person wouldn't get from "This sentence is false." to "Prohibit circularity." in a few short steps. How to prohibit circularity (whether through Russell's theory of types or simply chronologically - one theorem chronologically preceding another) is another matter entirely. The fact that circularity is to be avoided at all costs is entirely predictable. -- RichardKulisz

You seem to think that Goedel intentionally set out to play games with paradoxes. This is simply false; he was trying to find a way of preventing them, in furtherance of the Hilbert Program, and was initially just as appalled as you are by his discovery. However, he didn't try to run from it, either. In any case, both Church and Turing would later demonstrate even more crucial problems with mathematical formalism later, most of which are independent of the Incompleteness Theorem. -- JayOsako

By causing trouble, I refer to systems where it appears that a sentence is the only choice allowed (its negations are all inconsistent with the system), yet it remains unprovable from within the system.

In all the systems I know anything about, a sentence has only one negation. And in most systems (including the ones almost all working mathematicians use) if a sentence's negation is inconsistent with something then the sentence is provable from it. Unless you're using "inconsistent" to refer to some higher-level thing involving blurring of the boundary between the theory and the metatheory, in which case it seems that you don't find the troubles that causes quite so predictable as you said. :-) -- gjm

Do you recall the different schools of thought in mathematics? There were the Constructionists (who won out I think), the Formalists, and I think there was another one ... The trouble with "the set of all sets that do not include themselves" is its self-reference. By going the Constructionist route, a lot of self-reference is eliminated. -- rk

The constructivists did not win. Mathematicians often like constructive proofs when they are available, but hardly anyone these days takes constructivism seriously as a philosophy of mathematics. To some extent, the formalists won; to a greater extent, most working mathematicians just forgot about the issues and carried on as they always had. -- GarethMcCaughan

On the contrary, constructivism is very much alive and flourishing. -- TorkelFranzen

It's hardly mainstream, though. It's very common for mathematicians to use the axiom of choice whenever convenient, and this results in the existence of sets which can't be constructed - e.g. well-ordering for the reals, basis for the reals, unmeasurable sets. -- JG

I only encountered the terms once, many years ago, and I never quite understood the difference between constructivists and formalists at the time. You're entirely right, the constructivists did not win, but the logi(***?) lost big time. The notion that "the set of all sets" is meaningful is dead now and neither the constructivist nor the formalist school is friendly to the notion of "absolute truth" (what "truth" means colloquially). -- RichardKulisz

A while ago, I talked to someone taking philosophy of mathematics, and it seems the death of SetOfAllSets should be looked at carefully... discussion here has been moved there. -- JoshuaGrosse

When did it die? - It actually died, in so far as it did, with the birth of modern set theory. Cantor's ideas about transfinite cardinals showed that you should theoretically be able to build a bigger set than any given one, which rules that possibility out. But Goedel's work showed that the axiomatic set theory worked out precisely by Zermelo and Fraenkel isn't a definite word on the subject, and since then SetOfAllSets-type objects have reappeared under the name "class" in topics like CategoryTheory. That's not an answer, then, if it only died "in so far as it did"...

Another way to look at the Incompleteness Theorem is: the problem domain of mathematics cannot be resolved ("decided" suggests that there is an a priori right answer) by a finite set of axioms. Of course, this has the disadvantage of being comprehensible, thus showing the theorem to be trivial. Eh?

I'd be happy with an infinite set of axioms, though.

It depends what kind of infinity you're talking about. What's the biggest constructible transfinite number anyways? aleph_aleph_null?

There isn't a biggest constructible transfinite; once you have one, you can just take its power set. That's actually the problem with having a SetOfAllSets - if you could build it, you could build a bigger one.

What do you mean by "constructible"?

Derivable from an interesting set of axioms, like Peano's.

What does it mean for a number to be "derivable" from any given set of axioms? If you mean something like "can be proved to exist from the axioms", then Peano's won't do for constructing infinite numbers of any sort; they're only concerned with the integers. If you take something like the axioms of ZF set theory, then the answer is that there is no biggest one: you can always make a bigger.

You make it sound like, once we have integers, we're stuck! The funny thing is, though, that once we have integers, it's a tiny step to fractions, and from there, we can step to the reals. At any point (even with the integers) we can pick up polynomials, and once we have polynomials, we can make the leap to complex numbers. Somewhere in here, we can also contruct "infinite" numbers, either by resorting to limits, or by resorting to infinite series. And all this just scratches the surface of what you can do with integers.

My mistake then. But using the axiom of power set, you can construct aleph_n+1 from aleph_n, and by mathematical induction you can prove aleph_(aleph_null) but it's not clear to me how you would go about constructing something bigger.

Mathematical induction takes you as close as you want to infinite, but it doesn't let you get there. But in any case, once you did get aleph_(aleph_null) you could still just power set it again. See SetOfAllSets, though.

Oh, and one thing I just noticed. You said "a finite set of axioms" above. Goedel's theorem doesn't need the set of axioms to be finite. It needs to be simple in a particular sense, but it needn't be finite. I'm pretty sure that the system of "Principia Mathematica", which was the original target of Goedel's theorem, has infinitely many axioms.

As an aside, "constructible" actually means that the mathematical object in question can be proved to exist starting from a set of axioms that are accepted by the Constructionists. In particular, the set of accepted axioms excludes the principle of Tertium Non Datur (aka the law of the ExcludedMiddle), i.e. that to show a certain object exists, it suffices to show that its non-existence would lead to a contradiction.

GoedelsTheorem can not be proved in System S.

Rebecca Goldstein has a biography of Gödel (http://www.amazon.com/exec/obidos/tg/detail/-/0393051692?v=glance) that fills in much detail about Gödel's philosophy, his differences with Russell, and his friendship with Einstein. It's a good read.

One point that she makes is that in popularizing Gödel's work, pop philosophers have turned his work on its ear. Gödel's theorem is often cited in the context of limits -- as if Gödel "proved" that no absolute truth is possible. In fact, he did just the opposite. The claim of Gödel's peers was that a formal system could prove everything, in the absence of a connection to a real-world model. Rather than argue with them in the salons of Vienna (Gödel apparently abhorred debate), Gödel published his elegant proof that demonstrated that "truth" was, in Gödel's view, an external platonic reality that could not be fully described by ANY formal system.

Goldstein also offers a reasonably accessible discussion of Russell's paradox and its implications. Gödel was strongly influenced by Moritz Schlick (see http://en.wikipedia.org/wiki/Moritz_Schlick) and was greatly disturbed by his 1936 murder. I greatly enjoyed Goldstein's description of the intellectual "fabric" of Gödel's Vienna years. Many of the twentieth century's important logicians, philosophers, and mathematicians conversed, socialized, and debated during these years -- including (in addition to Gödel) LudwigWittgenstein, BertrandRussell, WillardVanOrmanQuine, and others.

According to philosophy professor DaleJacquette, Gödel's Theorem can be neutralized by using MeinongianLogic.

According to JeanYvesGirard, every other year comes another crook that "neutralizes" or "works around" Goedel. Fortunately for us mere programmers, Goedel's work was continued by Church and Turing, so such "proposals" can be subjected to a very simple test: try to write the solution to the HaltingProblem in the new "paradigm".

Done. I have managed to produce the formulation of a computation engine that can solve its corresponding halting problem and the corresponding logic has the expected property that the strong version of GodelsIncompletenessTheorem? (the one that given a system produces a problem it can't solve) produces a problem the system can solve.

{Good. Now post it here or on LambdaTheUltimate or in an academic journal, so that it can be subjected to peer review. Otherwise, it didn't happen.}

it's coming HyperBooleanTuringMachineDraft

GoedelsIncompletenessTheorem is in extreme contradiction with StringTheory, since it claims to be a theory of everything which incompleteness and infinity forbid. If StringTheory stopped claiming to be a theory of everything, or if it became just a model instead of a theory of everything, it would stand a small chance at succeeding. Infinity and incompleteness forbid a finite "everything". Infinity would be "anything" whereas string theory claims to be the theory of "every" thing. The theory of "any thing" is similar to saying "theory of infinity", which may be a contradiction or paradox itself, if it is not possible to have a theory of infinity or any thing.

CategoryMath