Timeline for Why do people say Gödel's sentence is true when it is true in some models but false in others?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 28, 2021 at 12:58 | comment | added | Timothy Chow | @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. | |
| Oct 27, 2021 at 23:26 | comment | added | Qfwfq | @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. | |
| Oct 27, 2021 at 22:27 | comment | added | Qfwfq | @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). | |
| Oct 27, 2021 at 18:14 | comment | added | user76284 | @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. | |
| Oct 27, 2021 at 16:55 | comment | added | Qfwfq | @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. | |
| Oct 26, 2021 at 8:36 | comment | added | user76284 | @Qfwfq believing "φ is true" is the same thing as having a ZFC proof of "N ⊨ φ" Consider φ = Con(ZFC). | |
| Oct 12, 2021 at 1:38 | comment | added | Timothy Chow | Let us continue this discussion in chat. | |
| Oct 12, 2021 at 0:24 | comment | added | Timothy Chow | @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. | |
| Oct 11, 2021 at 15:05 | comment | added | Timothy Chow | @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. | |
| Oct 11, 2021 at 12:22 | comment | added | Timothy Chow | @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. | |
| Oct 11, 2021 at 9:48 | comment | added | CouldntLoginToMyPreviousAcc | "mathematics comes first and formalization only after it" I think that's the "Platonic religion" Qfwfq was talking about. | |
| Oct 10, 2021 at 16:45 | comment | added | მამუკა ჯიბლაძე | 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, 2021 at 16:42 | comment | added | მამუკა ჯიბლაძე | 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, 2021 at 16:40 | comment | added | მამუკა ჯიბლაძე | 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, 2021 at 11:30 | comment | added | Timothy Chow | 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. | |
| Oct 10, 2021 at 11:23 | comment | added | Timothy Chow | @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. | |
| Oct 10, 2021 at 5:15 | comment | added | CouldntLoginToMyPreviousAcc | "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 | |
| Oct 10, 2021 at 3:28 | comment | added | Qfwfq | +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$". | |
| Oct 10, 2021 at 3:08 | comment | added | Timothy Chow | 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. | |
| Oct 10, 2021 at 2:53 | history | answered | Timothy Chow | CC BY-SA 4.0 |