29

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?

mrtaurho
  • 165
  • 8
    Many people do say "true in standard model". Sometimes it is implicit that the standard model is what they mean. – Wojowu Oct 09 '21 at 10:19
  • Wikipedia says "true but unprovable" and that's gotten me confused for a long time... guess you can't trust wikipedia. – CouldntLoginToMyPreviousAcc Oct 09 '21 at 10:23
  • This question is related to and answered by this: https://mathoverflow.net/questions/40209/how-to-reconcile-godels-theorem-with-the-completeness-of-the-predicate-calculus?rq=1 – CouldntLoginToMyPreviousAcc Oct 09 '21 at 10:24
  • If I understand correctly, Gödel himself proposed a Platonism philosophy, where the mathematical truths are different from being provable: https://plato.stanford.edu/entries/goedel/ – Z. M Oct 09 '21 at 10:35
  • 5
    I’m not a logician, but isn’t there a pretty straightforward answer to this question without a lot of philosophizing? The Gödel sentence is true if the theory it is the Gödel sentence for is consistent, right? So, if you believe the consistency of PA, you believe it’s Gödel sentence is true, and similarly for ZFC, right? – Aaron Bergman Oct 10 '21 at 11:36
  • @AaronBergman It was not obvious to me why the consistency of PA implies its $g$ is true. Because there are non-standard models of PA in which $g$ is false. Hence my original question. And now I understand when people say "$g$ for PA is true", they are really saying "$g$ for PA is true for some of PA's models, i.e., the standard ones. the ones that only deal with natural numbers. – CouldntLoginToMyPreviousAcc Oct 10 '21 at 13:14
  • I believe the statement is in Timothy Chow’s answer below and in JDH’s post referenced in the comments http://jdh.hamkins.org/are-all-godel-sentences-equivalent/. – Aaron Bergman Oct 10 '21 at 13:37
  • 7
    @Qfwfq I believe that your statement about other contexts in mathematics is just empirically false. Plenty of number theorists will happily affirm, "I believe that the Riemann hypothesis is true." They certainly don't mean that it's provable, and if you talk about standard structures and metatheories then they will just stare blankly in incomprehension at your religious jargon. – Timothy Chow Oct 11 '21 at 12:31
  • 4
    @Qfwfq Saying that the Gödel sentence is true amounts to saying that a certain Diophantine equation (that we can write down explicitly) does not have solutions. It is a simple arithmetic statement. I leave it to everyone to decide for themselves whether statements of this kind can be considered to be true or false in some objective way, or in some model that we can agree is the intended model of arithmetic. – Vladimir Reshetnikov Oct 11 '21 at 17:43
  • @Qfwfq Your anti-Platonist religion is stranger than the Platonist one, since it denies that there's a fact of the matter as to whether a Turing machine actually halts or not. See The Formalist Perspective in this article. – user76284 Oct 26 '21 at 08:25
  • Facts are relative. The fact that a Turing Machine halts (or not) is relative to something, according to an anti-Platnoist. – CouldntLoginToMyPreviousAcc Oct 27 '21 at 04:49
  • @Qfwfq I suggest you learn what a $\Pi^0_1$ sentence is. – user76284 Oct 27 '21 at 18:18
  • @CouldntLoginToMyPreviousAcc Right, that's a reductio ad absurdum. – user76284 Oct 27 '21 at 18:20
  • @user76284: I doubt my perplexity about Platonism has anything to do with technical aspects of syntax. But I won't continue the discussion inside this MO question: it was already lengthy (and perhaps a bit off topic for the site) and parts of it have been moved to chat by Timothy Chow. – Qfwfq Oct 27 '21 at 22:38
  • Edit: "have been moved to chat by the system". – Qfwfq Oct 27 '21 at 23:29

4 Answers4

48

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.

  • @AlessandroDellaCorte: Indeed, thanks for the catch! – Peter LeFanu Lumsdaine Oct 09 '21 at 11:56
  • 12
    +1. It would be a good idea to also be more precise about what you mean by "the Gödel sentence". There's a difference between the relationship between ZFC and the Gödel sentence for PA (for example) vs the Gödel sentence for ZFC itself. This could be related to the OP's confusion: are we justified in saying the Gödel sentence for ZFC is true? – Alex Kruckman Oct 09 '21 at 12:19
  • Just to check if I understand correctly: Godel sentence is provable in ZFC and therefore true from ZFC, which is a more powerful and standard axiomatic system of mathematics. Since ZFC is the standard, we simply say Godel sentence is true. – CouldntLoginToMyPreviousAcc Oct 09 '21 at 14:42
  • Regarding ZFC being the standard, how do mathematicians know ZFC is the right axiomatic system to use? Is it because most of the theorems provable from ZFC match our mathematical intuitions/expectations? Regarding unprovable statements of ZFC such as CH, if someone devices a novel axiomatic system which proves or disproves CH and proves all the other interesting theorems such as FLT, would it be a better system and can therefore replace ZFC? – CouldntLoginToMyPreviousAcc Oct 09 '21 at 14:52
  • 1
    @CouldntLoginToMyPreviousAcc (1) The acceptance of ZFC rests on multiple pillars, including the fact that most theorems proven in ZFC match our intuitions, as well as the fact that the axioms of ZFC match our intuitions, and that many other reasonable axioms systems are closely related to ZFC. (2) It's possible that a better axiom system could be found although (in a take I read somewhere on this website, maybe from JDH) it's very unlikely that mathematicians would ever accept a resolution of CH since we know so much interesting math conditional on CH or its negation. – Will Sawin Oct 09 '21 at 14:59
  • 3
    @CouldntLoginToMyPreviousAcc: See "Believing the axioms" by Maddy (https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf) – Sam Hopkins Oct 09 '21 at 16:56
  • 1
    A small correction: ZFC plus the hypotheses of Godel's incompleteness theorem imply the Godel statement. This is important because one of the hypotheses is that the theory is consistent, which ZFC might not be able to prove. – Christopher King Oct 09 '21 at 22:40
  • 3
    As Alex says, this answer makes sense if by "the Godel sentence" one means the Godel sentence for PA. But the OP didn't specify that. It's not at all clear to me that one can apply this same argument to the Godel sentence for ZFC. – Mike Shulman Oct 09 '21 at 23:18
  • @WillSawin, there is also Andreas Blass’s argument for accepting ZFC as an appropriate axiom system for current mathematics: https://mathoverflow.net/a/90945/44143 –  Oct 10 '21 at 08:29
  • One more question: what's the status of Gödel sentence for ZFC? Is it believed to be also true (but unprovable) or truly undecidable? – CouldntLoginToMyPreviousAcc Oct 10 '21 at 13:25
  • @MikeShulman: I’ve added a note about how this applies to the Gödel sentence for ZFC. I don’t see any essential difference in that case; if you think something’s different, could you elaborate on what? – Peter LeFanu Lumsdaine Oct 10 '21 at 15:35
  • 1
    I would just like to point out that it does not matter at all what the "standard model" is, it may even be different for each person. Let $M$ be whatever model you wish to carry out the argument in, for instance the one your brain imagines to be imagining. Read Gödel's paper as if it is all taking place in $M$. At the end of it, the paper will have convinced you that a sentence $g$ has been constructed which is true in $M$. The same goes for any other statement, there is nothing special here about Gödel's theorem. – Andrej Bauer Oct 10 '21 at 16:37
  • 1
    @CouldntLoginToMyPreviousAcc The Gödel sentence for ZFC is equivalent to "ZFC is consistent." Anyone who believes that ZFC is a plausible foundation for mathematics a fortiori believes that ZFC is consistent. Conversely, skeptics about infinite set theory typically don't believe that ZFC is consistent. As far as proving ZFC is consistent is concerned, we can't do this on the basis of ZFC itself. Whether this means that the consistency of ZFC is "truly undecidable" is a philosophical question. – Timothy Chow Oct 10 '21 at 18:19
  • @AndrejBauer: To forestall misunderstanding — When you say “any model”, do you mean “…of your meta-theory/foundations”, or “…of the object theory”? I guess you mean the former, in which case I agree entirely with your comment. But I think in speaking of the “standard model”, OP and others here mean “…of the object theory” or “…of arithmetic”, and for that, Gödel’s paper certainly doesn’t show that the Gödel sentence is true in any model — it shows, of course, precisely the contrary. – Peter LeFanu Lumsdaine Oct 10 '21 at 19:25
  • 1
    @PeterLeFanuLumsdaine: yes, I mean the meta-theory (hence my saying "the one your brain is imagining"), although it takes a bit of introspection to call it meta-theory. The bit about constructing a model $O$ of the object-theory in which Gödel's sentence $g$ fails, it is helpful to note that $O$ depends on $g$. – Andrej Bauer Oct 10 '21 at 20:27
  • Does godel's sentence rely on the axiom of choice? In other words, is ZF enough for it? – Oscar Smith Oct 11 '21 at 04:29
  • 2
    @OscarSmith The axiom of choice is not needed. In fact, almost nothing is needed to prove Gödel's incompleteness theorem. – Timothy Chow Oct 11 '21 at 15:12
  • 1
    Thanks for the clarification. I agree with what you wrote. My point was the same as what you said: when T is as strong or stronger as "the theory of informal mathematics", it is not justified to simply assert "The Godel sentence for T is true" without qualification. – Mike Shulman Oct 11 '21 at 15:13
16

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.

Timothy Chow
  • 78,129
  • 1
    In fact, all you really need to assume in the metatheory is that $T$ is consistent, not that $T$ is sound. In any reasonable metatheory, one can prove that $G$ is equivalent to the consistency of $T$; see this post by Joel David Hamkins for more details. But I think it's easier to grasp the main point if we allow ourselves to assume that $T$ is sound, which is what people are typically assuming anyway. – Timothy Chow Oct 10 '21 at 03:08
  • +1 for not talking about ancient religions :) - One other remark that could be made is that, while in the theory $T$ we're assessing the truth of $G$, in a meta-theory (such as ZFC) the sentence is not literally $G$ but the (fully unpacked version of) of something like "$\mathbb{N}\models G$". – Qfwfq Oct 10 '21 at 03:28
  • "so the fact that $T$ does not prove $G$ does not automatically rule out the possibility that $G$ is provable in the metatheory." Are the two $G$ exactly the same thing? I mean the former is $G$ expressed in the language of $T$, the latter is $G$ expressed in the language of a metatheory. When the latter is proved in the metatheory, all we can say is "$G$ is true in the metatheory" but not "$G$ is true in $T$", right? And when people say "$G$ is true but unprovable", it can be understood as "$G$ is true in some useful metatheory but unprovable in $T$"? @TimothyChow – CouldntLoginToMyPreviousAcc Oct 10 '21 at 05:15
  • @CouldntLoginToMyPreviousAcc You're right that technically there is a distinction; when I say "$G$ is provable in the metatheory" I am referring to $G$ as interpreted in terms of the standard integers, not to $G$ as a meaningless formal string. And yes, we cannot say "$G$ is true in $T$"—for the trivial reason that $T$ is a formal theory, so the phrase "true in $T$" doesn't make any sense. Finally, the answer to your last question is yes. – Timothy Chow Oct 10 '21 at 11:23
  • By the way, I think that the fact that you succumbed to the temptation to use the illegitimate phrase "true in $T$" illustrates my point that one tends to be interested in theories $T$ that are sound. If you keep in mind that in principle, $T$ could be inconsistent (in which case provability in $T$ has nothing to do with truth), that may help you avoid getting confused. – Timothy Chow Oct 10 '21 at 11:30
  • 2
    Concerning the last sentence: I believe most of the accounts of Gödel's theorem, including those emphasizing the philosophical/metamathematical implications, typically go not from a theory to its models. Rather, they follow the natural course encountered in mathematics: we have a mathematical structure we want to formally investigate, in the case at hand the set of natural numbers. We choose a formal system to argue about this mathematical structure, and start collecting facts about this structure that can be expressed in our formal system. We obtain a gradually growing body of knowledge. – მამუკა ჯიბლაძე Oct 10 '21 at 16:40
  • 1
    At certain stages we can extend this body of knowledge by adding to it formal consequences of what we already know. And Gödel's theorem asserts that occasionally we will inevitably need to either extend our formal system or use something else than just adding formal consequences. – მამუკა ჯიბლაძე Oct 10 '21 at 16:42
  • 1
    Sorry for this lengthy comment which is most probably also insufficiently accurate. I just wanted to say that if one agrees that mathematics comes first and formalization only after it, then there is no confusion about the status of truth anymore. I just could not figure out how to justify this in a shorter way. – მამუკა ჯიბლაძე Oct 10 '21 at 16:45
  • "mathematics comes first and formalization only after it" I think that's the "Platonic religion" Qfwfq was talking about. – CouldntLoginToMyPreviousAcc Oct 11 '21 at 09:48
  • 3
    @CouldntLoginToMyPreviousAcc Qfwfq's comments about "Platonic religion" are unclear so I can't say for sure how they relate to what მამუკა ჯიბლაძე said, but there is nothing religious or metaphysical about how the word true is used in mathematics. For example, it is true that if you append a symbol to a string then the string becomes longer. If asserting that appending a symbol to a string makes it longer is an illegitimate metaphysical article of faith, then we can't get off the ground. – Timothy Chow Oct 11 '21 at 12:22
  • 2
    @Qfwfq Trying to gloss "true" as "provable" is a recipe for all kinds of confusion, not to mention flying in the face of established usage in mathematical logic. "True in T" does not make any sense, except in Qfwfq-land. But the comment section is not the place for this hoary debate. – Timothy Chow Oct 11 '21 at 15:05
  • @Qfwfq No, this is not formalism. Nor is truth the same as provability of a sentence in the metatheory. This is not a philosophical difference; it's just wrong. But this comment section is not the place to hash this out. – Timothy Chow Oct 12 '21 at 00:24
  • @Qfwfq believing "φ is true" is the same thing as having a ZFC proof of "N ⊨ φ" Consider φ = Con(ZFC). – user76284 Oct 26 '21 at 08:36
  • @user76284: Ok, as for any other sentence $\varphi$ in the language of PA, the natural language assertion "Con(ZFC) is true" translates formally to: "$\mathbb{N}\models$Con(ZFC)", which is a sentence of ZFC (assuming ZFC is our metatheory here). We will also never get a ZFC proof of that sentence. Which is in line with the fact that we don't know whether ZFC is consistent. --- But why would your example be in tension with anti-Platonism? I think I might be missing your point. – Qfwfq Oct 27 '21 at 16:55
  • @Qfwfq The point is that Con(ZFC) is true in the same sense that Con(PA) is true, but ZFC cannot prove it. Yes, we do know that ZFC is consistent, because the von Neumann universe satisfies it (just like the natural numbers satisfy PA). If you don't think ZFC is consistent, why would you claim truth is equivalent to provability in ZFC? Why would you be using ZFC to define truth in the first place? Anything can be proved from an inconsistent theory, rendering your definition useless. – user76284 Oct 27 '21 at 18:14
  • @Timothy Chow: I see you didn't move to chat some of your replies to me. For readability sake, I think it'd be better if you moved to chat the whole thing (meaning: my comments inside this question and anybody's replies to me). – Qfwfq Oct 27 '21 at 22:27
  • @Timothy Chow: Oh, I thought those comments of mine were deleted/moved by you... I didn't take any action to delete them (that I'm aware of!) but something might have gone wrong when I used the mobile app. No problem. I'll delete stuff here that no longer makes sense, and I'll use the chat for potential future comments. – Qfwfq Oct 27 '21 at 23:26
  • @Qfwfq I have manually copied some of the above comments to the chat, and deleted some more of my own comments, since I really hope that the conversation can be moved to chat. – Timothy Chow Oct 28 '21 at 12:58
6

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.

  • 1
    Ha! Excellent. Somehow I missed that the OP started off by explicitly assuming consistency, like I missed the first sentence of the You are a bus driver puzzle. – Timothy Chow Oct 12 '21 at 00:33
  • "IF this logic system is consistent, THEN this logic system does not prove its Gödel sentence" Is this sentence provable in the metatheory or in the logic system it refers to? – CouldntLoginToMyPreviousAcc Oct 12 '21 at 02:12
  • Provability has always been clear to me: it's just a finite amount of symbol manipulation. To me, a Gödel sentence (for PA) is just many symbols grouped in some syntactically correct way. The sentence has no meaning unless we assign meaning to its underlying symbols. So claims like "GS is true" sounded to me like "GS is true under all interpretations", hence my confusion. – CouldntLoginToMyPreviousAcc Oct 12 '21 at 02:32
  • 1
    "IF this logic system is consistent, THEN this logic system does not prove its Gödel sentence" is provable basically anywhere you like. It's provable in the logic system it refers to, and also it's provable in any other reasonable metatheory you care to consider. The proof is so basic that it goes through wherever you like. – Sridhar Ramesh Oct 12 '21 at 03:26
  • 2
    If provability is clear to you, that's all that is going on. When people claim "X is true", all they are conveying is that they have a proof of X, in some theory they consider acceptable grounds for claiming things to be true (which is what people mean by "metatheory"). When people claim "X is true but unprovable (in system C)", what is going on is that their metatheory T proves X, but their metatheory T also proves "C does not prove X".

    Everything that's going on is, as you put it, "a finite amount of symbol manipulation". There's nothing else mystical going on.

    – Sridhar Ramesh Oct 12 '21 at 03:31
  • 2
    The language of nonstandard models perhaps ends up confusing this point. I think it would be easiest to understand the relevant dynamics focusing just on these brute syntactic things that you feel are clear. You should take "X holds in all models of logic system C" to mean exactly the same thing as saying "X is provable in logic system C". These might as well be synonymous phrases, for our purposes here. – Sridhar Ramesh Oct 12 '21 at 03:38
  • 2
    Saying "X is false in a nonstandard model of C, but is true in the standard model" is exactly the same as saying "X, but the system C I am interested in does not prove X". A person feels warranted to make this claim precisely when their metatheory T proves X, but also T proves "C does not prove X". – Sridhar Ramesh Oct 12 '21 at 03:39
0

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.

Stilez
  • 125
  • 1
    I downvoted the vagueness about which “logic systems” have these properties, the lack of examples, and the mischaracterization of the question: the question does not ask about “adding an axiom to make the sentence true or false”, but rather about different models in which it might be true or false. –  Oct 10 '21 at 08:13
  • "am a beginner, so this question may be naive" ..... 1) Not everyone understands the technicalities of axiomatic mathemetical/logic theory. But many have heard of Godels jncompleteness, even if not fully understanding it. There is a place for a simple explanation among the complex more accurate ones. 2) The OP in effect says you can add an axiom, whereby its no longer undecidable. A typical error, because that of course changes the axioms, and some other proposition will be undecidable, rather than the original. Typical error. This in simple terms explains that error, and why its so. – Stilez Oct 10 '21 at 08:58
  • @Stilez About item 2) in your comment: I didn't see anything in the question that "in effect says you can add an axiom". – Andreas Blass Oct 10 '21 at 21:13
  • I had in mind that OP, being a self.declared beginner, said "g can't be a logical consequence of the axioms, which means there are models of the system that make g false." I had in mind that, as they acknowledge the axioms dont allow g to be decidable, they might have in mind, logical extensions of the system, which would 1) be consistent with the existing system and 2) allow g to be clearly false, and wouldn't this contradict the whole idea. Thats a common beginner error, so its one I was addressing, why it wouldn't work that way, in simple terms. – Stilez Oct 11 '21 at 00:14