It's because it's a huge can of worms that leads to really grandiose claims that aren't supported by Godel's statements, of the sort the article is already beginning to make.
It also shifts the conversation into becoming fundamentally a philosophical question rather than a logical or mathematical one, which is okay, but considerably changes the table stakes of what background knowledge we need.
> If there are unprovable statements in any consistent set of axioms, might we also conclude there also be an unprovable but true statements?
That is one potential philosophical position. Another philosophical position is that there are no "true" axioms schemes, but rather that axiom schemes are always indefinitely extendable. Truth lies instead in how we choose to apply the axiom schema to the external world, which is outside the purview of Godel's Incompleteness Theorem. Both positions are supported by Godel's Incompleteness Theorem.
For example, do you believe that the Continuum Hypothesis (CH) is true? That is, although it is independent of ZFC, do you believe that objectively we are only allowed to use CH as an axiom or Not(CH) as an axiom. One of those must be objectively wrong. Some people do some people don't.
Likewise, do you believe that the imaginary numbers are "true?" That is the axioms that make them up are not artificial statements that somebody can up in pursuit of an abstract theory, but are immutable truths of the universe and that in fact you cannot choose an alternative axiomatization because it would be "wrong?" Some people some people don't.
What about the natural numbers?
There are many philosophical positions you can take on the notion of mathematical truth and the crucial thing is describing Godel's theorems with reference to truth suggests that Godel's theorems help decide among these notions of mathematical truth, when in fact what happens is that Godel's theorems stretch and shrink to accommodate different philosophical frameworks. The former is why I think a lot of people accord Godel's theorems a mystical status that makes it very difficult to have coherent discussions about them.
To pedagogically illustrate why the notion of truth can be confusing, I'll repeat two questions I've listed elsewhere which I think are good things to meditate on for first-time readers of Godel's Incompleteness theorems and explore why the often grandiose philosophical proclamations arising from Godel's theorems require very careful footing.
I answer them in my post history, but I would recommend you don't look at those before you've come up with answers yourself.
------Repost-----
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?).
dwohnitmok, I think you make a good point about Completeness missing out on the action in OP's post, which is nevertheless a good post and better than popular treatments. In fact, I remember thinking in class, "What, there is Completeness theorems as well as Incompleteness?" This is due to a similar phenomenon as we see with quantum mechanics in popular writing, where mostly the sensational, which aren't really sensational, is written.
In any case, my contribution here is something else: The most interesting part of the natural numbers object and its role in incomplete logical systems is to me the more humble notion of... unique prime factorisation.
If that had failed, so too would the Godel numbering system. I am not a number theorist, but this to me would be an interesting spin off from OP's post. The divisibility lattice is a good starting point, but apart from such basic constructions, the actual proof of unique prime factorisation to me is more historic than informative, and steps such as Bezout's Identity are just as "mythical" to me as Godel's Incompleteness Theorem, if we are using bad word choices. Conversely, numbers are just permutations on prime generators, but crucially, usually we start with addition before we start with multiplication.
Oof... what's the term for being sunk by the very thing that you're warning against?
I was using a very hand-wavy version of the word "truth" in my reply, trying to frame it in terms of how people talk about capital T Truth in informal philosophy rather than, say, model satisfability in model theory (which completely side-steps this question by assuming its resolution).
What I meant was to express a hypothetical anti-Platonist position. One version of mathematical Platonism is a belief that only some subset of "plausible" (i.e. those expressed by a consistent set of axioms) mathematical entities are real and it is the job of logician-philosophers to feel out just what those are. Of course they must appeal to extra-mathematical and extra-logical principles to do so, but that is after all why Platonism is a philosophy rather than a branch of mathematics. This is a simplified version of the philosophy that underlies some efforts to find "the one true set theory" that extends ZFC.
A hypothetical brand of anti-Platonism could argue that every consistent set of axioms is similarly real or unreal. There is no reason to choose one over the other. The only thing that has any objective reality to it is the mapping of those axioms to the real world. That you can do either correctly or incorrectly. Hence if we're talking about capital T Truth (i.e. the reality of the world) it is captured in that mapping, rather than the axioms themselves. Therefore, e.g. there's no point to trying to divine "the one true set theory." Just use whatever you find useful.
Regardless my overall point is that these are all matters of philosophy that cloud the particulars of what is going on with Godel's incompleteness theorems, often by exaggerating their consequences.
Godel's theorems have philosophical ramifications, but then again so do basically all theorems given the right framing.
It is nonetheless true that Godel's theorems are a particular focal point of discussion around mathematical philosophy (but again one which has surprisingly few ramifications for mathematics as a whole) and a very fruitful one at that. I'm not dismissing the idea of having a philosophical discussion around it, only cautioning that it requires a deep understanding of all the seemingly paradoxical statements that it presents which defy attempts to concisely state its philosophical ramifications.
My point at the beginning of all of this is that I disagree with the pedagogical choice of a lot of introductory posts to the incompleteness theorems to mix in that philosophical content at the beginning. You can always do it later after first understanding a lot of seemingly paradoxical statements that arise from Godel's theorems (such as the ones I offered concerning Conway's Game of Life and the consistent system that proclaims the inconsistency of its subpart).
However, by presenting the philosophical parts up front, that tends to be the thing that people latch onto rather than the inner workings of the theorems (which are extremely important to understand to make sure subsequent philosophical conclusions are coherent), and they latch onto the everyday, woolly meanings of the words "prove" and "truth" rather than their more precise counterparts in the theorems.
The exaggeration in the article I'm referring to is
> For example, it [Godel's incompleteness theorem] may mean that we can’t write an algorithm that can think like a dog...but perhaps we don’t need to.
To address this specific point, Godel's incompleteness theorems have little to say on this point. I think the assumed chain of logic is "algorithms rely on a computable listing of axioms" -> "any such listing must have truths that are unprovable in it" (the Godel step) -> "dogs perceive truth" -> "there are certain things dogs perceive that cannot ever be derived by an algorithm."
But leaving aside the plausibility of the non-Godelian steps in that chain, it's relying on a subtle simplification of what "truth" means that severely complicates the chain. Again, I would highly recommend thinking over the Conway Game of Life and inconsistent consistent theory problems. Those two problems demonstrate that "any such listing must have truths that are unprovable in it" is often an over-simplification (okay so I have a system S and the sentence "S is inconsistent" is consistent with S if S is consistent. What is true here?)
This is very similar (and indeed the similarity runs deeper due to connections between computability and logic) to analogous arguments with the halting problem/Rice's Theorem.
"Rice's theorem says that we cannot prove any abstract property about any program" -> "Static analysis attempts to prove abstract properties about programs" -> "Static analysis is impossible."
Or similar arguments that use the halting problem to argue that Strong AI is impossible.
More broadly though this sort of "anti-mechanistic" viewpoint appears all over the place in discussions about Godel's theorems to the point that the Stanford Encyclopedia has a whole section dedicated to it that plainly states "These Gödelian anti-mechanist arguments are, however, problematic, and there is wide consensus that they fail." https://plato.stanford.edu/entries/goedel-incompleteness/#Gd...
Having seen some of those arguments I am very inclined to agree with the encyclopedia here.
Thank you for your clarity. This discussion chain may have kicked of an existential crisis. I think you might have exposed me to a Lovecraftian horror. The article and your discussion have been, if not mind altering, very much mind expanding.
I can't say I've followed all of the nuance in your (argument?) comments. I do know I'm going to be chewing on this for a while. I've come to grips with horror of saccades, fascinating to learn about new ways my mind, uh, decides what is true.
In any case, I appreciate your long thoughtful responses. May not mean much to you, but for at least one reader, it means a lot to me.
It also shifts the conversation into becoming fundamentally a philosophical question rather than a logical or mathematical one, which is okay, but considerably changes the table stakes of what background knowledge we need.
> If there are unprovable statements in any consistent set of axioms, might we also conclude there also be an unprovable but true statements?
That is one potential philosophical position. Another philosophical position is that there are no "true" axioms schemes, but rather that axiom schemes are always indefinitely extendable. Truth lies instead in how we choose to apply the axiom schema to the external world, which is outside the purview of Godel's Incompleteness Theorem. Both positions are supported by Godel's Incompleteness Theorem.
For example, do you believe that the Continuum Hypothesis (CH) is true? That is, although it is independent of ZFC, do you believe that objectively we are only allowed to use CH as an axiom or Not(CH) as an axiom. One of those must be objectively wrong. Some people do some people don't.
Likewise, do you believe that the imaginary numbers are "true?" That is the axioms that make them up are not artificial statements that somebody can up in pursuit of an abstract theory, but are immutable truths of the universe and that in fact you cannot choose an alternative axiomatization because it would be "wrong?" Some people some people don't.
What about the natural numbers?
There are many philosophical positions you can take on the notion of mathematical truth and the crucial thing is describing Godel's theorems with reference to truth suggests that Godel's theorems help decide among these notions of mathematical truth, when in fact what happens is that Godel's theorems stretch and shrink to accommodate different philosophical frameworks. The former is why I think a lot of people accord Godel's theorems a mystical status that makes it very difficult to have coherent discussions about them.
To pedagogically illustrate why the notion of truth can be confusing, I'll repeat two questions I've listed elsewhere which I think are good things to meditate on for first-time readers of Godel's Incompleteness theorems and explore why the often grandiose philosophical proclamations arising from Godel's theorems require very careful footing.
I answer them in my post history, but I would recommend you don't look at those before you've come up with answers yourself.
------Repost-----
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?).