9 ms·

If you're uninitiated and simply want to grok where true-but-unprovable comes from, I recommend: https://www.quantamagazine.org/how-godels-incompleteness-theore

If you're uninitiated and simply want to grok where true-but-unprovable comes from, I recommend: https://www.quantamagazine.org/how-godels-incompleteness-theorems-work-20200714/ https://www.quantamagazine.org/how-godels-incompleteness-the... Wolchover is masterful here. The layers of abstraction keep piling up, and I had to read the last part more than a couple of times to really get it, but then you have it.

dwohnitmok 6y ago
The article plays a little fast and loose with language > For example, Gödel himself helped establish that the continuum hypothesis, which concerns the sizes of infinity, is undecidable, as is the halting problem The continuum hypothesis is definitely not "undecidable" in the same way that the halting problem is undecidable. Though there are deep connections behind the two, the two notions of "undecidability" (logical independence in the former and Turing machine computability in the latter) are very different. Also, > He also showed that no candidate set of axioms can ever prove its own consistency. This is powerful as a limiting result, but it has little direct impact for philosophy, because you wouldn't trust the consistency result of a system you suspect might be inconsistent to begin with because inconsistent systems can prove anything. So saying "my axioms prove themselves consistent" shouldn't have increased your trust in those axioms to begin with in the absence of the incompleteness theorems. I'm not really a fan of "true-but-unprovable" as short-hand the incompleteness theorems, because that hinges a lot on what kind of logic system you're in and how that logic system defines "truth" (taken at face value, how do we know that Godel's incompleteness theorem is "true?"). I prefer rather to pose two questions to reflect on that I think illuminate Godel's incompleteness theorems some more. Most modern logical systems (e.g. first-order logic and its various extensions and variants) equate unproveability with logical independence. So with that in mind, here's two questions. First, Conway's Game of Life: Conway's Game of Life seem like they should be subject to Godel's incompleteness theorems. It is after all powerful enough to be Turing-complete. Yet its rules seem clearly complete (they unambiguously specify how to implement the Game of Life enough that different implementation of the Game of Life agree with each other). So what part of Game of Life is incomplete? What new rule (i.e. axiom) can you add to Conway's Game of Life that is independent of its current rules? Given that, what does it mean when I say that "its rules seem clearly complete?" Is there a way of capturing that notion? And if there isn't, why haven't different implementations of the game diverged? If you don't think that the Game of Life should be subject to Godel's Incompleteness Theorems why? Given that it's Turing complete it seems obviously as powerful as any other system. Second, again, in most logical systems, another way of stating that consistency is unproveable is that consistency of a system S is independent of the axioms of that system. However, that means that the addition of a new axiom asserting that S is either consistent or inconsistent are both consistent with S. In particular, the new system S' that consists of the axioms of S with the new axiom "S is inconsistent" is consistent if S is consistent. What gives? Do we have some weird "superposition" of consistency and inconsistency? Hints (don't read them until you've given these questions some thought!): 1. Consider questions of the form "eventually" or "never." Can those be turned into axioms? If you decide instead to tackle the question of applicability of the incompleteness theorems, what is the domain of discourse when I say "clearly complete?" What exactly is under consideration? 2. Consider carefully what Godel's arithmetization of proofs gives you. What does Godel's scheme actually give you when it says it's "found" a contradiction? Does this comport with what you would normally agree with? An equivalent way of phrasing this hint, is what is the actual statement in Godel's arithmetization scheme created when we informally say "S is inconsistent?" At the end of the day, the philosophical implications of Godel's incompleteness theorems hinge on whether you believe that it is possible to unambiguously specify what the entirety of the natural numbers are and whether they exist as a separate entity (i.e. does "infinity" exist in a real sense? Is there a truly absolute standard model of the natural numbers?).
- braindongle 6y ago
  Who cares about the philosophical implications of the theorems? Philosophers! The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All. The literature on Gödel and philosophy is gargantuan, for some reason. Wasn't it summed up well by Wittgenstein? Paraphrasing: "Who cares about your contradictions?" Well said. Also not the topic Wolchover's article. Math people can make the same move: "Who cares about your philosophizing?"
  - dwohnitmok 6y ago
    > The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All. Sort of. Whitehead's contributions to universal algebra are still relevant and universal algebra is still a thriving field of study for mathematical logic. Although perhaps you mean "algebra" in a more informal sense? Again, the conclusion of the article is a bit strong. > Gödel’s proof killed the search for a consistent, complete mathematical system. The consistency half doesn't make sense. (EDIT: I get it now, see the last sentence of this paragraph) There was never a search for a consistent mathematical system in the sense that Godel destroyed because again a system that can prove its own consistency has no positive value in evaluating the consistency of that system (Godel's big contribution here is contributing a strong negative result, if it could prove its own consistency you're pretty screwed). EDIT: On reflection I see that the sentence probably means to tie consistency to completeness rather than as a stand-alone quality. That makes more sense. As for mathematicians, their reactions to Godel's incompleteness theorems overall are probably similar to "Who cares about your incompleteness theorems?" (there's a reason Russell and Whitehead are known primarily for being philosophers first and mathematicians second and why often times there is distinction between logicians like Godel and other mathematicians). Most mathematicians don't think about the foundations of mathematics because it is (perhaps surprisingly) largely irrelevant to the day-to-day work of mathematicians. Indeed the vast majority of mathematics is very resilient to changes in its underlying foundations. To interpret Godel's incompleteness theorems requires a healthy dose of at least mathematical logic that can start veering quite close to mathematical philosophy. An example from the article: > However, although G is undecidable, it’s clearly true. G says, “The formula with Gödel number sub(n, n, 17) cannot be proved,” and that’s exactly what we’ve found to be the case! Well no, that's not true in certain senses. Indeed in a larger axiomatic system subsuming the current system that corresponds to G, it is completely consistent to state that G is provable and that its statement is provable (see my example of S'), i.e. there are Godel numbers that correspond to both a proof of G and to a proof of its content. To interpret that statement that way requires certain philosophical commitments to the correspondence between a Godel number and truth, which not everyone would accept (do you accept the truth of the new axiom introduced by S'? Why then do you accept the truth of the statement "S is consistent?" and vice versa). "In striving for a complete mathematical system, you can never catch your own tail." This on the other hand I think is a very good informal description of what's on with Godel's incompleteness theorems. Focus on the incompleteness not on truth. That's why I'm not a fan of using the word "truth" when talking about Godel's incompleteness theorems. I am in fact deeply sympathetic to your desire to separate philosophy from Godel's incompleteness theorems. I prefer to clearly delineate between its logical properties in mathematical logic and its philosophical implications and using the word "truth" by necessity muddles the two. FINAL EDIT: I am being perhaps a bit too harsh on the article. I think it does a fine job of describing the arithmetization of the incompleteness theorems. But if someone else reading this also decides to create an informal guide to Godel's incompleteness theorems, please please please don't use the word "truth" and "true" or at least separate it out into its own section on philosophy.
dvt 6y ago
Just going to echo @dwohnitmok here in saying that this is a pretty 'meh' article. Understanding Godel's First Incompleteness Theorem is actually very accessible, I wrote about it a few years ago[1]. His second is much more involved and laymen won't have the required tools to grasp it. In my opinion, the easiest way to understand it is probably using Löb's Theorem, but that's neither here nor there. Either way, I'm of the opinion that arithmetic coding is very confusing and shouldn't be used to introduce people to Godel. [1] https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers/ https://dvt.name/2018/03/12/godels-first-incompleteness-theo...
- irontinkerer 6y ago
  Per the end of your article, have you started writing about the 2nd theorem yet?
  - dvt 6y ago
    I did (https://dvt.name/2018/04/11/godels-second-incompleteness-theorem-programmers/ https://dvt.name/2018/04/11/godels-second-incompleteness-the...) -- but like I mentioned, it's not very accessible and I don't think it's a particularly good explanation, either (although I've yet to find one I really like, to be honest).
- krick 6y ago
  I'm not sure this is equivalent to Gödel's theorem. Actually, I'm not sure this is a correct proof of anything at all, merely a sort-of demonstration of Richard's paradox. First, for reference, let me quote First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (from Wikipedia) Now back to your post. Obviously, f' is not in T and it is not computable. But neither is T. It is incomputable merely by being the list of computable functions, which we cannot construct because of halting problem and stuff like that. And your definition of f' relies on having T. So we don't in fact have seen "statement f'". So, the direct connection between Gödel's theorem and your construct is not obvious to me, because first is about constructable, but unprovable statements, and second seems to be a faulty (i.e. mathematically uninterpretable) construct itself.
jjcc 6y ago
May I suggest that "true" in "true-but-unprovable" means from God's eye or in a higher level system but not in current system because "unprovable"（in current system only) means it's not really true in current system? Correct me if I'm wrong in this context.
- hilbertseries 6y ago
  You are wrong. Godel in fact showed precisely that there are unprovable statements in any consistent set of axioms. In fact it’s equivalent. The only systems in which every statement is provable are inconsistent. Consistent here meaning that statements cannot be proven to be both true and false from axioms.
  - dpierce9 6y ago
    This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are provable). For example, the predicate calculus you learn in Logic 101. Formal systems become provably incomplete when they are able to express arithmetic (e.g., Peano axioms).
  - jjcc 6y ago
    I'm not contradictory to your statement. Or your explanation hasn't touch my potential flaw if exists. Let me put in this way: There is at least some "thing" that can not be proved without cause inconsistency. To avoid the inconsistency to prove the "thing" which become true we need to create a high order system in which then the "thing" is truth but also cause the same dilemma in the new bigger system that new "thing" will show up that need another high order system. So it's correct that no system can contain all truth while keeping consistent. This is the point you want to express in your statement, right? (Actually it's Godel theorem in plain English itself) What I try to say is: if its not provable in current system so it can not be called true within current system. I could be wrong at this part but not what you tried to explain which I already agree.
  - jfarmer 6y ago
    There are two other conditions/premises that, arguably, play a bigger role in Gödel's theorems: 1. The theory must be strong enough to do a certain amount of arithmetic 2. The axioms of the theory must be computably enumerable So, you can have relatively weak theories in which the incompleteness results don't hold. A major example here is comes from Gödel's _completeness_ theorem (notice "completeness" not "INcompleteness") which says: in first-order logic a statement is true if and only if its provable. You can also have strong theories whose axioms are not computably enumerable. Start with something like the Peano axioms and consider the set of all true statements in that theory. We can take any set we want as axioms, so what if we take the set of all true statements in Peano arithmetic as our axioms? Now every valid "proof" is one line long since what was previous a theorem is now an axiom, but we've kicked the can down the road. How do we figure out whether something is an axiom in this new system or not? This latter system is called "true arithmetic" Gödel's incompleteness theorems don't apply there, either.
hogfeldt 6y ago
Thanks for the link, it was a joyful read.

dwohnitmok 6y ago

The article plays a little fast and loose with language > For example, Gödel himself helped establish that the continuum hypothesis, which concerns the sizes of infinity, is undecidable, as is the halting problem The continuum hypothesis is definitely not "undecidable" in the same way that the halting problem is undecidable. Though there are deep connections behind the two, the two notions of "undecidability" (logical independence in the former and Turing machine computability in the latter) are very different. Also, > He also showed that no candidate set of axioms can ever prove its own consistency. This is powerful as a limiting result, but it has little direct impact for philosophy, because you wouldn't trust the consistency result of a system you suspect might be inconsistent to begin with because inconsistent systems can prove anything. So saying "my axioms prove themselves consistent" shouldn't have increased your trust in those axioms to begin with in the absence of the incompleteness theorems. I'm not really a fan of "true-but-unprovable" as short-hand the incompleteness theorems, because that hinges a lot on what kind of logic system you're in and how that logic system defines "truth" (taken at face value, how do we know that Godel's incompleteness theorem is "true?"). I prefer rather to pose two questions to reflect on that I think illuminate Godel's incompleteness theorems some more. Most modern logical systems (e.g. first-order logic and its various extensions and variants) equate unproveability with logical independence. So with that in mind, here's two questions. First, Conway's Game of Life: Conway's Game of Life seem like they should be subject to Godel's incompleteness theorems. It is after all powerful enough to be Turing-complete. Yet its rules seem clearly complete (they unambiguously specify how to implement the Game of Life enough that different implementation of the Game of Life agree with each other). So what part of Game of Life is incomplete? What new rule (i.e. axiom) can you add to Conway's Game of Life that is independent of its current rules? Given that, what does it mean when I say that "its rules seem clearly complete?" Is there a way of capturing that notion? And if there isn't, why haven't different implementations of the game diverged? If you don't think that the Game of Life should be subject to Godel's Incompleteness Theorems why? Given that it's Turing complete it seems obviously as powerful as any other system. Second, again, in most logical systems, another way of stating that consistency is unproveable is that consistency of a system S is independent of the axioms of that system. However, that means that the addition of a new axiom asserting that S is either consistent or inconsistent are both consistent with S. In particular, the new system S' that consists of the axioms of S with the new axiom "S is inconsistent" is consistent if S is consistent. What gives? Do we have some weird "superposition" of consistency and inconsistency? Hints (don't read them until you've given these questions some thought!): 1. Consider questions of the form "eventually" or "never." Can those be turned into axioms? If you decide instead to tackle the question of applicability of the incompleteness theorems, what is the domain of discourse when I say "clearly complete?" What exactly is under consideration? 2. Consider carefully what Godel's arithmetization of proofs gives you. What does Godel's scheme actually give you when it says it's "found" a contradiction? Does this comport with what you would normally agree with? An equivalent way of phrasing this hint, is what is the actual statement in Godel's arithmetization scheme created when we informally say "S is inconsistent?" At the end of the day, the philosophical implications of Godel's incompleteness theorems hinge on whether you believe that it is possible to unambiguously specify what the entirety of the natural numbers are and whether they exist as a separate entity (i.e. does "infinity" exist in a real sense? Is there a truly absolute standard model of the natural numbers?).

braindongle 6y ago
Who cares about the philosophical implications of the theorems? Philosophers! The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All. The literature on Gödel and philosophy is gargantuan, for some reason. Wasn't it summed up well by Wittgenstein? Paraphrasing: "Who cares about your contradictions?" Well said. Also not the topic Wolchover's article. Math people can make the same move: "Who cares about your philosophizing?"
- dwohnitmok 6y ago
  > The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All. Sort of. Whitehead's contributions to universal algebra are still relevant and universal algebra is still a thriving field of study for mathematical logic. Although perhaps you mean "algebra" in a more informal sense? Again, the conclusion of the article is a bit strong. > Gödel’s proof killed the search for a consistent, complete mathematical system. The consistency half doesn't make sense. (EDIT: I get it now, see the last sentence of this paragraph) There was never a search for a consistent mathematical system in the sense that Godel destroyed because again a system that can prove its own consistency has no positive value in evaluating the consistency of that system (Godel's big contribution here is contributing a strong negative result, if it could prove its own consistency you're pretty screwed). EDIT: On reflection I see that the sentence probably means to tie consistency to completeness rather than as a stand-alone quality. That makes more sense. As for mathematicians, their reactions to Godel's incompleteness theorems overall are probably similar to "Who cares about your incompleteness theorems?" (there's a reason Russell and Whitehead are known primarily for being philosophers first and mathematicians second and why often times there is distinction between logicians like Godel and other mathematicians). Most mathematicians don't think about the foundations of mathematics because it is (perhaps surprisingly) largely irrelevant to the day-to-day work of mathematicians. Indeed the vast majority of mathematics is very resilient to changes in its underlying foundations. To interpret Godel's incompleteness theorems requires a healthy dose of at least mathematical logic that can start veering quite close to mathematical philosophy. An example from the article: > However, although G is undecidable, it’s clearly true. G says, “The formula with Gödel number sub(n, n, 17) cannot be proved,” and that’s exactly what we’ve found to be the case! Well no, that's not true in certain senses. Indeed in a larger axiomatic system subsuming the current system that corresponds to G, it is completely consistent to state that G is provable and that its statement is provable (see my example of S'), i.e. there are Godel numbers that correspond to both a proof of G and to a proof of its content. To interpret that statement that way requires certain philosophical commitments to the correspondence between a Godel number and truth, which not everyone would accept (do you accept the truth of the new axiom introduced by S'? Why then do you accept the truth of the statement "S is consistent?" and vice versa). "In striving for a complete mathematical system, you can never catch your own tail." This on the other hand I think is a very good informal description of what's on with Godel's incompleteness theorems. Focus on the incompleteness not on truth. That's why I'm not a fan of using the word "truth" when talking about Godel's incompleteness theorems. I am in fact deeply sympathetic to your desire to separate philosophy from Godel's incompleteness theorems. I prefer to clearly delineate between its logical properties in mathematical logic and its philosophical implications and using the word "truth" by necessity muddles the two. FINAL EDIT: I am being perhaps a bit too harsh on the article. I think it does a fine job of describing the arithmetization of the incompleteness theorems. But if someone else reading this also decides to create an informal guide to Godel's incompleteness theorems, please please please don't use the word "truth" and "true" or at least separate it out into its own section on philosophy.

dvt 6y ago

Just going to echo @dwohnitmok here in saying that this is a pretty 'meh' article. Understanding Godel's First Incompleteness Theorem is actually very accessible, I wrote about it a few years ago[1]. His second is much more involved and laymen won't have the required tools to grasp it. In my opinion, the easiest way to understand it is probably using Löb's Theorem, but that's neither here nor there. Either way, I'm of the opinion that arithmetic coding is very confusing and shouldn't be used to introduce people to Godel. [1] https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers/ https://dvt.name/2018/03/12/godels-first-incompleteness-theo...

irontinkerer 6y ago
Per the end of your article, have you started writing about the 2nd theorem yet?
- dvt 6y ago
  I did (https://dvt.name/2018/04/11/godels-second-incompleteness-theorem-programmers/ https://dvt.name/2018/04/11/godels-second-incompleteness-the...) -- but like I mentioned, it's not very accessible and I don't think it's a particularly good explanation, either (although I've yet to find one I really like, to be honest).
krick 6y ago
I'm not sure this is equivalent to Gödel's theorem. Actually, I'm not sure this is a correct proof of anything at all, merely a sort-of demonstration of Richard's paradox. First, for reference, let me quote First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (from Wikipedia) Now back to your post. Obviously, f' is not in T and it is not computable. But neither is T. It is incomputable merely by being the list of computable functions, which we cannot construct because of halting problem and stuff like that. And your definition of f' relies on having T. So we don't in fact have seen "statement f'". So, the direct connection between Gödel's theorem and your construct is not obvious to me, because first is about constructable, but unprovable statements, and second seems to be a faulty (i.e. mathematically uninterpretable) construct itself.

jjcc 6y ago

May I suggest that "true" in "true-but-unprovable" means from God's eye or in a higher level system but not in current system because "unprovable"（in current system only) means it's not really true in current system? Correct me if I'm wrong in this context.

hilbertseries 6y ago
You are wrong. Godel in fact showed precisely that there are unprovable statements in any consistent set of axioms. In fact it’s equivalent. The only systems in which every statement is provable are inconsistent. Consistent here meaning that statements cannot be proven to be both true and false from axioms.
- dpierce9 6y ago
  This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are provable). For example, the predicate calculus you learn in Logic 101. Formal systems become provably incomplete when they are able to express arithmetic (e.g., Peano axioms).
- jjcc 6y ago
  I'm not contradictory to your statement. Or your explanation hasn't touch my potential flaw if exists. Let me put in this way: There is at least some "thing" that can not be proved without cause inconsistency. To avoid the inconsistency to prove the "thing" which become true we need to create a high order system in which then the "thing" is truth but also cause the same dilemma in the new bigger system that new "thing" will show up that need another high order system. So it's correct that no system can contain all truth while keeping consistent. This is the point you want to express in your statement, right? (Actually it's Godel theorem in plain English itself) What I try to say is: if its not provable in current system so it can not be called true within current system. I could be wrong at this part but not what you tried to explain which I already agree.
- jfarmer 6y ago
  There are two other conditions/premises that, arguably, play a bigger role in Gödel's theorems: 1. The theory must be strong enough to do a certain amount of arithmetic 2. The axioms of the theory must be computably enumerable So, you can have relatively weak theories in which the incompleteness results don't hold. A major example here is comes from Gödel's _completeness_ theorem (notice "completeness" not "INcompleteness") which says: in first-order logic a statement is true if and only if its provable. You can also have strong theories whose axioms are not computably enumerable. Start with something like the Peano axioms and consider the set of all true statements in that theory. We can take any set we want as axioms, so what if we take the set of all true statements in Peano arithmetic as our axioms? Now every valid "proof" is one line long since what was previous a theorem is now an axiom, but we've kicked the can down the road. How do we figure out whether something is an axiom in this new system or not? This latter system is called "true arithmetic" Gödel's incompleteness theorems don't apply there, either.

hogfeldt 6y ago

Thanks for the link, it was a joyful read.