In Gödels Incompleteness theorem what is the notion of truth?

Question

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?

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 denote the standard model of Q (and its domain) and say that a sentence is true if it is true in (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) ∈ ( x ): 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 formula (i.e., a formula all of whose quantifiers are bound) defining Proof(S) in .

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

Choose a Gödel sentence G such that . Since Q is sound, G is true if is true. Note that S, as an extension of Q, is -complete meaning that every true 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) = is the formalized statement of the consistency of S.

The Simplest Version of the Argument for G's Truth

1. is true [Assumption]
2. [(1), -completeness of S]
3. [(1), definition of Pr[S]]
4. [(3), definition of G]
5. [(2), (4)]
6. 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): , 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. [Assumption]
2. [(1), Rfn(S)]
3. [(2), definition of G]
4. [(1), (3)]
5. [(1)-(4)]
6. [(5), version of _reductio ad absurdum]
7. [(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 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 . It then relies on the familiar analysis of truth simpliciter as truth in . So, "is true" in the first argument above can be cashed out as "is true in " 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.