The way I understand it, Gödel took Russel's and Whitehead's Principia Mathematica (PM) and mapped strings of symbols from PM onto the integers, their Gödel numbers.

He then constructed, within PM, a class of integers that correspond to the Gödel numbers of (syntactically valid) PM statements that are derivable within PM.

Lastly, he constructed one statement that said the statement with the Gödel number G does not belong to that class (where G wasn't given explicitly but implicitly, compressed), and he constructed this statement in such a way that G was just the Gödel number for that statement.

Thus, either there was a derivation of that statement in PM, which would make it a false statement and show that false statements were derivable in PM, or the statement would be true but not derivable. This would make PM incomplete or inconsistent.

I hope I got it right this far.


Gödel thus proved an unprovable statement. Well, a statement not provable in PM, but PM was supposed to be powerful enough to capture all meaningful mathematics and an analogous proof can be shown to exist for every system more powerful than PM.

How is the proof above possible if it is not possible within PM?

  • People are still chewing on this chestnut. I don't recall the practical use of it though.
    – Scott Rowe
    Commented Jul 27, 2022 at 16:33
  • 1
    @ScottRowe Some mathematicians claim Godel's (1st) incompleteness theorem is the foremost pure math achievement in the 20 century, and perhaps its practical use is morally reminding us to be humble in our ambitious metaphysical axiomatizations as envisioned by Hilbert, of course other practical uses include stimulating logic pluralism and research programs with emphasis on computer science applications not seen in previous centuries compared to other traditional math branches... Commented Jul 28, 2022 at 2:52
  • 1
    Perhaps high level talks addressing your central puzzle for such an intricate technical aspect won't make you ever crystal-clear about what's really going on unless you prove it yourself from first line to Q.E.D, as the saying goes devils are in details. The sentence Con(PA) is provably equivalent to Godel sentence G per his 2nd incompleteness thm, so you'd think consistency of similar arithmetic system cannot be proved by itself, but surprisingly some seemingly strong arithmetic formal system such as Willard's Self-verifying theories Commented Jul 28, 2022 at 3:09
  • 1
    Thus this hints the unintuitive mysterious incompleteness of PA which is fully capable of encoding and representing (capturing) its own provability has something to do with the totality of multiplication of natural numbers satisfying distribution axioms together with addition. Some number theorists envisioned non-rigidity of multiplication in some Teichmüller inter-universe to try to shed further light on it... Of course since Godel sentence G is independent of PA, you can always form a new system PA+G (or PA+¬G) to easily and trivially prove G (or ¬G, respectively) to your satisfaction... Commented Jul 28, 2022 at 3:32
  • 1
    The "G-numbered" statement is unprovable in PM but can be proved in a "larger" system; but then Godel's construction applies, and for the larger system we will found a new unprovable statement (different from the previous one). This means that you are right: the "dream" implicit in PM's project: to find the ultimate system that will formalize all of mathematics was unteneable. Commented Jul 28, 2022 at 7:00

2 Answers 2


"Godel thus proved an unprovable statement" - this is not quite the case, as you yourself recognize in the lines following. Rather, Godel proved that there exists an undecidable statement for every formal system which meets certain reasonable properties. Such a proof is in reality a meta-proof, that is, a proof in the meta language about the proof-system (here, our formal theory).

If our metalanguage meets the same "reasonable properties", we can construct a corresponding undecdiable statement for it too. But such a proof will have to proceed in a meta-meta- language and so forth. In particular, the undecidable statement is relativized to the formal system in question.

So there is no contradiction between a meta-proof existing and Godel's result as applied to the language or the meta-language. In particular, if PM is powerful enough to act as a metalanguage for itself, we can formulate Godels' result for PM as an object language.

  • Thanks, that's nice and succinct. So, a metalanguage M can prove non-derivability of a statement S in a language L. Does that always work? Can I have an automated reasoner and a meta-reasoner and the meta-reasoner can always check, before using the reasoner to try to prove a statement, whether the reasoner will succeed? Something tells me it's not that simple---I'm missing something. Commented Jul 28, 2022 at 7:32
  • this works when S is the Godel sentence, and does not hold generally. If it did, we would be able to "decide" whether a proof exists. But in fact a large class of problems are undecidable (in fact, this gives an alternate way of proving Godel's theorem)
    – emesupap
    Commented Jul 28, 2022 at 17:19

Godel started with the liar paradox: "This statement is not true." But "true" is a rather difficult concept to define for axiomatic proof systems (see Tarski's undefinability theorem) so Godel modified it to the alternative "This statement is not provable." "Provable" is often used as a substitute for "true" in axiomatic proofs. This second statement, too, is a bit too vague for formal logic - what do you mean by "provable"? We have lots of different sets of axioms, lots of different rules of deduction. So Godel adds more detail: "This statement is not provable in the formal proof system Y." where "Y" stands for some set of axioms and deductive rules.

Now we can encode the formulas as numbers and the deductive rules as arithmetical relationships between them, so "provable in the formal proof system Y" becomes an arithmetical fact about numbers. Now we add one final trick to get the self reference, and construct a Godel number X that encodes the statement "Statement X is not provable in the formal proof system Y." We have managed to encode the nearest relation of the liar paradox as an arithmetical property of a particular number.

If the number X has this arithmetical property, then we can use our meta-understanding of what the arithmetical property means to conclude statement X is provable in Y, and use our meta-understanding of the encoding scheme to know that what we've proved is that statement X is unprovable in Y. This is inconsistent, and thus we know that formal proof system Y is inconsistent.

If the number X does not have this arithmetical property, then we use our meta-understanding of the arithmetical property to conclude X is unprovable. We use our meta-understanding of the encoding scheme to see that this is exactly what X says, and thus we meta-conclude that X is true, but Y is incomplete. There are true statements that it cannot prove.

In short, a logic powerful enough to talk about itself (such as Principia's arithmetic) is either incomplete or inconsistent. Because a logic powerful enough to talk about itself can express a version of the liar paradox, and the only way to avoid the paradox from destroying it is for the paradoxical statement to be unprovable.

The critical thing about all this is that the meta-system we use to interpret the numbers can be different from the system Y specified in the statement. If we try to use Y itself, and succeed, then the statement we've just proved is false and Y is inconsistent. If we use a different meta-system to do the interpretation, there is no such objection. "'Statement X is not provable in the formal proof system Y.' is provable in formal proof system Z." is perfectly fine.

So as a human, we can informally use human intuition as proof system Z, and know that the statement is true. Some people have tried to use this to demonstrate the superiority of humans over algorithms, because the human proof machine Z can always prove it, but formal system Y inevitably fails. This is not so.

We can see this in another classic logical conundrum: the paradox of the unexpected hanging. In this problem, the judge tells the condemned prisoner that he will be hanged at dawn during the following week but the execution will be a surprise to the prisoner. The prisoner reasons that it cannot happen on the last day, else it wouldn't be a surprise. He would know it was coming at sunrise the previous day. So it can't happen on the second to last day either, because he would know the sunrise before. And so on. And so it cannot happen on any day. The prisoner is safe! And thus it comes as a complete surprise to him when he is taken out at dawn and hung on Tuesday.

What we're doing here is making a statement like "The date of the hanging is not predictable by the prisoner." This has the same shape as our Godel sentence. X is the date of the hanging, 'provable' is replaced by 'predictable', and Y is the prisoner. Prisoner Y cannot predict the day of the hanging (his knowledge of the future is necessarily incomplete), because that creates an inconsistency. But the executioner can.

In general, we can exclude any category of prover just by including them in the statement to be proved. "This statement cannot be proved by humans." could, in theory, be proved (informally) by a machine. The statement "This statement cannot be proved by Nigel." can be proved by everyone except people called 'Nigel'. And so on. Humans are not excluded. They're just less bothered by the liar paradox rendering their reasoning system inconsistent.

Godel sentences can only be made precise if you specify what system is doing the proof, and so we always have an escape hatch in that we can always choose to prove it using a different formal system. We can thus prove that it is unprovable, because we are using two different meanings/definitions of 'proof'.

  • Yeah, I'm not bothered at all by realizing that I am incomplete and inconsistent. That's life!
    – Scott Rowe
    Commented Jul 28, 2022 at 10:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .