Why do people say Gödel's sentence is true when it is true in some models but false in others?

Question

I am a beginner, so this question may be naive.

Suppose we have a (sufficiently strong) consistent first order logic system. Gödel's first incompleteness theorem says there exists a Gödel sentence $g$ which is unprovable, and its negation is also unprovable. By Gödel's completeness theorem, $g$ can't be a logical consequence of the axioms, which means there are models of the system that makes $g$ false. So my question is: then why do people say $g$ is true when viewed outside the system?

PS: apparently there are "non-standard models" that makes $g$ false according to wikipedia, then why don't people say $g$ is true in standard models, which is more accurate? Also, do non-standard models work with natural numbers anymore?

Answer 1

When we say the Gödel sentence is true, we mean exactly the same thing as when we say the Fundamental Theorem of Arithmetic is true, or Fermat’s Last Theorem, or any other theorem in mathematics. We mean that we’ve proven it, using our standard consensus principles for reasoning about mathematical objects. And when we talk about natural numbers — as in FTA, FLT, or the Gödel sentence — we mean the actual natural numbers, not arbitrary models of PA.

With FTA or FLT, we don’t usually even question that. The reason we look at Gödel’s sentence in other models of PA isn’t because of any difference or subtlety in what the statement means — it’s just a difference in why we’re interested in it. That difference comes back to the question of what principles we’re using in our proofs.

Most of the time, we just take those “standard principles” as an implicit background consensus, and don’t mention them explicitly. But with our logicians’ hats on, we may want to be more explicit about them. Most of the time, they’re assumed to be ZFC set theory or something closely equivalent. So we can refine our statement that “the FTA is true” (or FTA, the Gödel sentence, etc) to “in ZFC, we have shown the FTA is true”, or more formally “ZFC proves FTA”.

And then to further refine it, we can ask: did we really need the whole power of ZFC, or does some weaker logical system suffice? So we can ask whether these theorems are provable in PA, or any other logical theory T that has a way of talking about natural numbers. And only then can we start asking about whether these statements may hold in some models of T and fail in others. Which is an interesting question — and especially because in the case of the Gödel sentence, we can show it holds in some models and fails in others — but it’s very much a secondary one, and doesn’t affect the original primary meaning of the statement. And it depends entirely on what theory T is under consideration.

The one subtlety to note here is that if we’re talking about “PA proves FTA” and “ZFC proves FTA”, these can’t quite be formally the same statement “FTA”, since one must be written in the formal language of arithmetic, the other in the language of set theory. What’s happening here is that the ZFC-version of “FTA” is an translation of the PA-version of FTA in ZFC, using ZFC’s set of natural numbers. This translation is what “the standard model” means. But it’s just part of giving a more refined analysis of the logical status of these statements — it doesn’t mean that every time we do any elementary number theory in ZFC, we should feel obliged to add “in the standard model”. The whole point of a standard model is that it’s standard — it’s just giving the language of arithmetic its usual meaning within ZFC (or other ambient foundation). You can equally well take “FTA” to be the PA-statement and view the ZFC-version as its interpretation under the standard mode, or take “FTA” to be the ZFC-statement and view the PA-version as a transcription of it into the language of arithmetic. The former is more common in logic, but the latter is arguably closer to mathematical practice.

So overall: It’s completely accurate to just say “The Gödel sentence is true”, in the same sense that we mean when we say any other mathematical statement is true or false. But if we want to refine that statement to a sharper one, then what we should say is “ZFC proves the Gödel statement [in the standard model of arithmetic].” — the part that really sharpens the statement is specifying “ZFC”, not the mention of the standard model. Similarly, when we say that it is unprovable (or fails in some models), we need to be clear which theory we’re talking about provability in, or models of.

Edit. I’ve assumed we’re talking of the Gödel sentence for PA, or some similar theory of arithmetic; but the same applies with the Gödel sentence for ZFC, or any other theory $T$. In Gödel’s theorem, we assume $T$ comes equipped with an interpretation of the language of arithmetic, and its Gödel sentence $G_T$ is a priori a sentence of arithmetic, that then gets (in the proof of Gödel’s theorem) interpreted into $T$. So again what it means when we say $G_T$ holds is no different in principle from what it means when we say FTA or FLT holds — it means “reasoning in the normal mathematical way, we can prove $G_T$ holds (in the natural numbers)”. So there’s no difference from before what it means for $G_T$ to hold. And there’s a difference, but a straightforward one, in whether we can show $G_T$ holds: If $T$ is a theory that we can prove consistent (so e.g. PA would be such a theory, if we’re working ambiently in something like ZFC), then using that, we can prove unconditionally that $G_T$ holds. If we can’t prove $T$ is consistent (e.g. if $T$ is ZFC itself, or something stronger), then all we can prove is: If $T$ is consistent, then $G_T$ holds.

Answer 2

There are several distinct issues to be aware of.

First, there is the question of the meaning of "true in a model" versus being simply "true" (or "true simpliciter" if you like Latin). Once one realizes that it is possible to build different mathematical structures in which the Gödel sentence (or indeed any sentence in the formal language of arithmetic) can be interpreted in different ways, it might seem that, to avoid ambiguity, it is always necessary to specify which interpretation I have in mind when I say that the sentence is true or false. Technically there is some chance of confusion, but when it comes to sentences of arithmetic, it is always assumed that "true" without further qualification means "true when interpreted in terms of the standard integers."

The more subtle question is, when people study some arithmetic theory $T$ and say that the Gödel sentence $G$ for $T$ is "true," what justification do they have for claiming that $G$ is true? At first glance, it might seem that such a claim is unwarranted. Conventionally, in mathematics, we feel justified in confidently asserting that something is true if (and only if) we can prove it. But if we're studying $T$, then we are typically interested in understanding what can be proved on the basis of $T$ itself. $G$ is specifically constructed so as to be unprovable in $T$ (unless $T$ is inconsistent) so it seems particularly confusing to confidently assert that $G$ is true when we (apparently) can't prove $G$.

The first point to recognize is that when we're trying to decide whether we are justified in asserting that $G$ is true (equivalently, whether we can prove $G$), what is relevant is the metatheory in which we are working, rather than the theory $T$ itself. When we're proving Gödel's theorem, we're reasoning about $T$, and whether we can prove this or that statement about $T$ depends on what metatheoretical principles we allow ourselves. The metatheory need not bear any particular relationship to $T$ itself, so the fact that $T$ does not prove $G$ does not automatically rule out the possibility that $G$ is provable in the metatheory.

Fine, you might say, but what if $T$ is something like PA, which also happens to be a perfectly good system for performing metatheoretical arguments? Can't we declare that our metatheory is also PA, and in that case, isn't it the case that we have no warrant for declaring (in the metatheory) that $G$ is true?

The answer is yes. You might indeed be working in some metatheory which doesn't prove $G$. Nothing in the proof of Gödel's theorem actually requires claiming that $G$ is true. You are perfectly within your rights to work within some weak metatheory in which $G$ cannot be proved, meaning that you don't have any real justification for asserting that $G$ is true.

"But wait," you say, "now I'm more confused than ever. I swear that I've read lots of accounts in which the truth of $G$ is asserted as fact. Now you're telling me that such a claim isn't warranted?" Well, I didn't quite say that. I said that you might be working in some metatheory which doesn't prove $G$. In many situations, though, you're studying a theory $T$ that hasn't been randomly plucked out of thin air; $T$ is being considered as a plausible candidate for the foundations of mathematics, and in particular, it is plausible that the theorems of $T$ are true (i.e., that $T$ is sound). For example, if $T$ were obviously inconsistent, you wouldn't be interested in studying it, would you? You also probably wouldn't consider $T$ to be a serious candidate for the foundations of mathematics if (for example) $T$ disproved Fermat's Last Theorem. So in your metatheory, you probably want to assume—even though strictly speaking you don't have to—that $T$ is sound. And from the assumption that $T$ is sound, we can easily prove $G$: if $G$ were false then $G$ would be provable in $T$, and the soundness of $T$ would imply that $G$ is true, which is a contradiction. This is why accounts of Gödel's theorem—at least, those which emphasize the philosophical/metamathematical implications—typically say that $G$ is true.

Answer 3

In your question, you start off saying "Suppose we have a (sufficiently strong) consistent first order logic system. Gödel's first incompleteness theorem says there exists a Gödel sentence 𝑔 which is unprovable...".

You have made here a supposition, that the logic system you are studying is consistent. This supposition is the very one that the logic system you are studying may not be able to prove. You, having made that supposition, are therefore in a position to claim certain things to be true which the logic system itself may not prove.

This is how it can come to be that you claim something is true even though the logic system you are studying may not prove it. (And to say there are models of a logic system where a sentence is false is just a roundabout way of saying that the logic system does not prove the sentence.)

---

Keep in mind, Gödel's incompleteness theorem can be framed without making this consistency supposition in the first place. Indeed, it would be much easier to see the matter clearly and avoid such "Moore's paradox" issues if people ordinarily framed the Gödelian phenomenon without that supposition. "IF this logic system is consistent, THEN this logic system does not prove its Gödel sentence". "IF this logic system is consistent, THEN this logic system does not prove its own consistency". This is the Gödelian phenomenon, and this sentence is readily provable (aka, true in all models). There is no danger of paradox once phrasing things in these terms, even if you make the natural choice to consider the same logic system as both metatheory and object theory.

The best attitude to take about the Gödel sentence by default is to refrain from calling it true and to refrain from calling it unprovable (in the sense of unprovability in the particular logical system it references). Instead, simply note that its truth entails its unprovability and vice versa, whether or not it is true and whether or not it is provable. In some particular contexts, you may go beyond that, but in general, that entailment is all there is to say.

Answer 4

In simple terms, it is true in this sense:

If you specify a logic system S1 by giving its axioms, there will be a Gödel sentence G1 that cant be decided within it. So the axioms cant be strong enough to prevent an undecidable proposition existing.

When you ask about adding an axiom A1 to make that sentence true or false, you are changing the axiomatic system we are discussing. You are now discussing S1+A1, call that system S2.

Its true that your original Gödel sentence G1 is now no longer undecidable in S2. Its clearly either true or false. But there will now exist a * different * Gödel sentence G2 that is undecidable in S2.

Gödels first incompleteness theorem states that however you try to strengthen S1, however many new axioms you bolster it with, its still incomplete. There will ALWAYS be a sentence Gn that is undecidable in your updated logic system Sn.

Answer 5

This question is rather old now, but I wanted to provide a different perspective. I think the above Model Theoretic answers are good, but they may give one the impression that one isn't at all justified to say that the Godel sentence corresponding to some suitable extension of ZF (say ZFC) isn't 'true' in some sense, but there is a sense in which this is justified, it is just not possible to use model theoretic language alone to see this.

The arguments given here are essentially a more high level overview of the arguments presented in Introduction To Meta-Mathematics by Stephen Kleene, and are treated more thoroughly there. Specifically, for a quick reference for most of the statements necessary for this argument, and another high level overview, see Chapter XI $\S$ 60, but a completely formal proof is basically impossible to give succinctly, so the rest of the book is highly recommended to gain a complete understanding.

To start, I will appeal to the history of the subject. The initial idea motivating Godel to prove his incompleteness theorems was the program of Hilbert that all mathematics could be 'carried out' using a single formal system. We can sort of break this down into two goals, although I don't know if the mathematicians of that time explicitly thought about this way:

1. Find a definition of computation that encompasses all possible computations
2. Find a formal system that can decide all possible true mathematical statements

The mathematicians of the time, I suspect, implicitly assumed that 1 and 2 were basically equivalent, and as a result, we often think about Godel's incompleteness theorems as the complete failure of Hilbert's program, because 2 turned out to be false. But in fact, looked at from a different perspective, it can be seen as halfway a success, since as far as we know 1 has a unique solution.

The solution is, as you may have already suspected, the notion of General Recursion, or Turing Computability. And as a result, the closest thing we got to Hilbert's original idea was not a mathematical statement, but a philosophical one: the Church Turing Thesis. Although this technically remains a philosophical claim, the point is that

• The Church Turing Thesis can be stated as a formal logical axiom in our meta-theory, and from this axiom we can show that the Godel statement is 'true' for any theory, even though it is not provable in said theory
• Despite it being a philosophical claim, it is extremely well motivated, since its formal statement is equivalent to assuming there is a decision procedure for deciding the validity of a proof (the equivalence of which I will go over later in this answer), which I think most 21st century mathematicians would agree is a very reasonable assumption. Its status as a dicey assumption comes from a time before computers became as ubiquitous as they are today.

As a result of this notion of computability and this thesis, we can give a (very) informal argument that "there are true statements that aren't provable" without invoking model theory or the independence of certain axioms.

Essentially, the argument relies on the insolubility of the halting problem (of which I am assuming the reader is already familiar). We will get to how this relates to the Godel sentence afterward. It goes like this:

In 'physical reality', we know that every algorithm we run will either halt or it will not. In this sense, intuitively, there is an 'absolute truth' of this fact (that notably does not rely on any concept of a model). However, we know that in a consistent theory that is 'bound' by Turing computability but is a powerful enough language to ask whether any algorithm halts or it doesn't, there will be some algorithm $M$ for which it does not have an answer. But since every algorithm halts or it doesn't, one of the statements "$M$ halts" or "$M$ does not halt" must be true but not provable. And that essentially completes the argument.

However informal this argument may be, one can hopefully see that it is extremely reasonable to expect that our meta-theory (corresponding to 'physical reality') has as a provable statement that every algorithm we run will either halt or it won't (even without the law of excluded middle, it seems reasonable to expect that we should be able to prove this in the constructive cases).

Moreover, 'being bounded' by Turing Computability can be suitably formalized.

The way in which it is formalized relies on a not-so-easy to see, but provably true statement, that:

(1) every General Recursive predicate (function from $\mathbb{N}^n \to 2$) is a predicate in the formal system presented by Godel in his original paper

(meaning in particular that it has a total recursive decision procedure for the validity of proofs).

In my opinion, this fact is the crowning achievement of the early 20th century logicians, and is to some degree lost under the more modern model theoretic view of this subject.

As a result of (1), we can formalize the Church Turing Thesis in a very nice way: that a consistent theory has a decision procedure for deciding the validity of its proofs.

Why does this correctly capture our intuitive notion of the Church Turing Thesis? Its because from this, we can argue that if the above is true, then every predicate is general recursive in the sense that we can algorithmically decide its truth value on some input if and only if it is provable.

The argument goes informally as follows and relies on (1) above:

Assume that that $S$ is a statement in some consistent theory $T$ such that there is an algorithm deciding if $x$ is a proof of $S$. Then by (1), there is a recursive predicate $P$ in Gödel's formal system such that $P([S], x)$ if and only if $x$ is an encoding of a proof of $S$.

But then, note that the predicate $p(S) = \exists x, P([S], x)$ is therefore general recursive, since we can simply enumerate the possible proofs $x$. Thus, $S$ is essentially 'general recursive'. In particular, if $\rho$ is a predicate in $T$, then we can run a program that computes $\rho(n)$ for some constant $n$ of the theory that does not halt if and only if $\rho(n)$ is independent in $T$.

That completes the argument

In essence, the above shows that there is an algorithm computing any predicate if validity of proofs is recursively decidable. Moreover, from the above argument, those who are familiar with certain proofs of the insolubility of the halting problem may be starting to see how the insolubility of the halting problem implies the undecidability of the Gödel sentence $G$.

Formally, the Gödel sentence is the statement $G = \lnot (\exists x, P([G], x))$. This is classically thought as "this statement is not provable", but the above discussion may hopefully indicate why this can also be thought of "this algorithm does not halt". Essentially there is an injective map between logical statements and algorithms, assigning a statement to an algorithm that outputs its proof. Then we follow the classic argument: If $G$ halts, then it is provable, contradicting itself, but on the other hand, if $G$ does not halt, then there is no proof it doesnt.

Therefore, we know in the metatheory, that if the theory in which $G$ is stated is consistent, then the only option is that $G$ does not halt, but the theory cannot prove that.

So just as a quick recap:

The model theoretic view is illuminating, but it is not the whole picture. The classical argument was not merely model theoretic, but also was intimately tied with the search for a universal method of computation. The above argument shows that if the Church Turing thesis is true (formally, the thesis that there is an algorithm in the Turing computable sense deciding validity of proofs) then in any reasonable meta-theory, and powerful enough theory $T$ expressible in that meta-theory, there is a statement that is true in the meta-theory that is not provable in $T$, and this statement does in essence correspond to the Godel sentence.

This means that this applies to basically any powerful enough meta-theory and consistent theory expressible within it, including ZFC, and not just specific cases such as Peano arithmetic.

However, all of this is predicated on the acceptance of the Church Turing thesis, but hopefully I have argued well that this is not an unreasonable assumption in the above sense. There are many more thorough arguments of course, a lot of them a bit less formal than the above, but the bottom line is that if it weren't the case, then formal mathematics would look very very different from what we know today.

I refer the reader again to Meta-mathematics by Kleene for the best argument I have seen.