The entry on Gödels Incompletenss theorem in Wikipedia says:

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,[1] but not provable in the theory (Kleene 1967, p. 250).

My understanding of Gödels theorem is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established ( a formal sentence being true iff every interpretation of it in every model is true). However the quote above says that a statement is true but not proveable.

Is this notion of truth different from model-theoretic truth?

The sketch of the proof in the article above doesn't establish a sentence that is true but that it is undecidable (neither proveable or refutable - note this is different from another notion of undecidability in computability).

Is a better characterisation of Gödels incompleteness theorem, in mathematical terms at least, is that there are undecidable statements in a sufficiently powerful proof system (can at least prove the theorems of PA)?

To give some context to the proof, if I've followed it correctly:

The Gödel sentence is: there is a sentence p such that p<=>not BGp where BGp means that the sentence p has a proof. Now this Gödel sentence has a proof. But the sentence says p is true <=> p has no proof.

It looks from this, that there is an internal notion of truth to the proof system that is used, but which is considered only formally when we think of the proof system as being a formal system. Is this correct?

  • Yes, I think an aspect of this or a variant on it is possibly one of the curious 'upshots' of the theorem. --Though again not an expert, my understanding is that there are necessarily unprovable statements which in some cases we do 'know synthetically' that they're true.
    – Joseph Weissman
    Jun 14, 2013 at 14:38
  • 1
    Thats what I'm trying to pin down. I'm aware of the model-theoretic notion of truth. But it doesn't seem to use it. The question is where is it sneaked in. Jun 14, 2013 at 14:44
  • @MöziburUllah Dö I really have tö keep föllöwing yöu tö cörrect yöur cöntinuöus misspellings öf Gödel? You obviously are intrigued by his theorem, please consider spelling his name right. (Unless your keyboard is broken, in which case I'll stick around.) Also consider using the godel tag, which, indeed, has its own spelling trouble. :)
    – user3164
    Jun 14, 2013 at 17:31
  • @Gugg: ok, point taken. My keyboard ain't broken, but I've no idea how to put on an umlaut - and I'd rather not copy & paste all the time. Jun 14, 2013 at 17:38
  • @MoziburUllah Fair enough! If you have one like mine (Mac), then press alt+u, release, press o.
    – user3164
    Jun 14, 2013 at 17:41

1 Answer 1


We have various proofs demonstrating the truth of the Gödel sentence. I'll present an argument given here.

Notational Preliminaries

First, fixing notation. I will use square brackets ([ ]) where I would normally subscript the character within the brackets. Let Q denote Robinson arithmetic and let S denote an arbitrary but fixed recursive consistent extension of Q. Let nat nums denote the standard model of Q (and its domain) and say that a sentence is true if it is true in nat nums (NOTE: it looks like we have your answer here; yes it is the standard notion of truth-in-a-model. At least, that is the notion used in at least one formalization of the proof. I'll go a bit further to show how we recognize the truth of the Gödel sentence.). For any formula p, let's reserve the bolded version, p, to stand for the Gödel number of p.

Next, Proof[S] = {(m, n) ∈ (nat nums x nat nums): n = p for some formula p and m is the Gödel number of a proof in S of p}

Proof[S](x, y) is to be a delta formula (i.e., a formula all of whose quantifiers are bound) defining Proof(S) in nat nums.

Pr[S](y)= quantifierx Proof[S](x, y), this is a sigma formula, where a sigma formula is a delta with an initial block of existential quantifiers (this block is allowed to be empty, so, every delta formula is a sigma formula; the converse, however, obviously does not hold).

Choose a Gödel sentence G such that godel sentence. Since Q is sound, G is true if no proof is true. Note that S, as an extension of Q, is sigma-complete meaning that every true sigma sentence is provable in S.

Finally (and boy did it take a long time to get to "finally"), let F denote the formal contradiction, and Con(S) = consistency is the formalized statement of the consistency of S.

The Simplest Version of the Argument for G's Truth

  1. enter image description here is true [Assumption]
  2. enter image description here [(1), sigma-completeness of S]
  3. List item [(1), definition of Pr[S]]
  4. List item [(3), definition of G]
  5. List item [(2), (4)]
  6. List item is true [reductio ad absurdum (1)-(5)]

This shows the unprovability of the Gödel sentence. You can turn it into a formal proof of G by dropping the references to truth and utilizing the Local Reflection Principle, abbreviated LRP. The principle runs as follows:

Rfn(S): enter image description here, where p is a sentence (i.e., a well-formed formula with no free variables).

Let S' be the result of extending S to include LRP. We can then modify the above proof into a formal proof of G within S':

  1. enter image description here [Assumption]
  2. enter image description here [(1), Rfn(S)]
  3. enter image description here [(2), definition of G]
  4. enter image description here [(1), (3)]
  5. enter image description here [(1)-(4)]
  6. enter image description here [(5), version of _reductio ad absurdum]
  7. enter image description here [(6), definition of G]

The author of the linked article, György Serény, gives us the following informal statement of the argument just presented:

Let us consider a sound theory, that is, one in which provability implies truth and suppose that G is a sentence that is true just in case it is unprovable. Now, let us assume that G is provable. Then, by the soundness of the theory, it is true. Therefore, by its definition, it is unprovable, contradicting the assumption. Consequently, it cannot be provable. Thus G is unprovable. But then, again by its definition, it must be true.

This informal argument does utilize the notion of "truth", but it isn't explicit that it is concerned with model-theoretic truth. I suspect, however, that it is. The reason I suspect this is because he appeals to the soundness of the theory. Generally soundness is stated as the conditional enter image description here and I don't know how else to interpret the double turnstile other than as the model-theoretic notion of truth. This bears on your initial point of confusion:

My understanding of Gödel's theorem is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established ( a formal sentence being true iff every interpretation of it in every model is true). However the quote above says that a statement is true but not provable.

Since the argument assumes the soundness of the system under consideration (in the formal version the assumption of soundness is captured by LRP), it establishes a link between provability and truth (and, if I am right to think that the double turnstile is to be read is model-theoretic truth, it establishes a link between provability and model-theoretic truth). Furthermore, the arithmetical machinery at work in the proofs makes explicit appeal to the standard model of S, namely nat nums. It then relies on the familiar analysis of truth simpliciter as truth in nat nums. So, "is true" in the first argument above can be cashed out as "is true in nat nums" and that seems to pretty explicitly invoke model theory.

Well, this is far longer than I expected it to be, but hopefully this answers your question.

  • 1
    Thanks Dennis for such a detailed answer. It does look like model-theoretic truth is involved. It goes to show that one shouldn't rely on wikipedia to give a proof sketch that mentions all the salient points. Jun 14, 2013 at 20:42
  • This does lead to another question what happens if we insist on using model-theoretic truth (I think the actual term for this is logical validity) instead of truth in the standard model? In first-order logic this is moot as all models are categorial but in higher logics they're not... Jun 14, 2013 at 21:47
  • @MoziburUllah "Logical validity" is, I think, ambiguous between semantic validity (truth in all models) and syntactic validity (provable from an empty premise set). I don't think you would want to use truth in all models whatsoever since we're interested in whether G is a truth of arithmetic and not of logic. This question actually spurred me to ask a question on Math.SE which you might be interested in, should it get any useful answers.
    – Dennis
    Jun 14, 2013 at 22:38
  • I've also asked this question in there too! Peter Smith answer complicates your own - he avers that there are actually two proofs of Godels theorem, one sound & the other syntactic. I prefer your terms semantic & syntactic validity to logical validity which is the one Peter Smith used. Jun 14, 2013 at 22:49
  • 1
    It turns out the Rosser trick eliminates the use of omega-consistency in the syntactic proof, at the cost of turning Godels sentence to a Godel-Rosser sentence. See Mumerts answer to my question. Jun 14, 2013 at 23:33

You must log in to answer this question.

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