I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem, and even the original proof is sketched in a very approachable manner, striking a very good balance between getting across all crucial ideas, and skipping most of the distracting technical aspects (which are important and interesting, but I think only to mathematicians, haha). Great job all around.
Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason:
The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Russell's Paradox). Gödel numbers (and in the author's case Lisp expressions) leave out the order of a proposition with the consequence that the Diagonal Lemma **cannot** be used to construct the proposition *I'mUnprovable*.
Furthermore, existence of the proposition I'mUnprovable contradicts the following fundamental theorem of provability that goes all the way back to Euclid:
I'm going to need someone to come along and write up a layman's summary of this article. :) Does it change the end result of Gödel? Or is it basically the equivalent of saying what some restricted programming languages are doing, that we can get "good enough" results and not have these problems by restricting what we can do in the language?
I thought I replied to this post, but I guess not and my reply ended up being a top-level reply, which is just as well. I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap.
1. Please don't bring the notion of truth into an introductory explanation (such as in the section "Power of Numbers" or in the short intro to "Hilbert's Program"). It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable." Just stick to incompleteness and consistency at a syntactic level instead of appealing to truth, that is respectively the ability to always add new axioms and the lack of syntactic contradictions.
2. The lack of a system S's ability to prove its own consistency is not interesting by itself since we would not trust a proof from a potentially inconsistent system. Hence it is not, in a sense, terribly interesting that we require an infinite tower of increasingly stronger systems to prove the consistency of S and themselves. Rather the interesting direction goes the other way. S cannot prove the consistency of stronger systems, which means we cannot have a "minimal" system we use to explore the consistency of all other systems (again subject to some nuance).
> I thought I replied to this post, but I guess not and my reply ended up being a top-level reply, which is just as well.
Sorry for the confusion. We detach comments that are replies to the top comment but don't respond to anything specific that that comment said. This is standard moderation. Sometimes we post that we did this (https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...), but not always.
We do this because users often post replies to the top comment on a page that aren't really replies. Sometimes they do that because they want to get their comment higher on the page (so-called topjacking). Of course that's not always the case.
Both of your posts are fine (except for the fact that they duplicate one another) but they are replies to the article, not to anything that the top comment (https://news.ycombinator.com/item?id=25116881) specifically says. Indeed your sentence "I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap." makes it quite clear that your reply is to the article, not xyzzyz's comment. That's great! But the appropriate level for such a comment is the top level of the thread.
Poking through your history, why do you quibble on the word truth so often? Do we not agree there are statements that are true? Do we not agree there are provable true statements ? If there are unprovable statements in any consistent set of axioms, might we also conclude there also be an unprovable but true statements?
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?).
Thank you, reading this comment and some of yours further down, thinking about the topics you set out, was very interesting.
To offer possibly a comment to yours about the notion of "truth", in the article posted, when I read "true" (e.g. in the 1st paragraph of chapter Hilbert's Program) and next to it "false", I immediately made reference in my mind to the true/false duality of programmers. I think that helped in understanding the article, but coupled with a footnote with your details would certainly help the reader think further on the topic.
The [Gödel 1930] "completeness theorem" is *false* for the
foundational theories of Computer Science because these
theories are inferentially incomplete, that is, not every
proposition can be proved or disproved.
As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference.
Instead our confidence in the consistency of a powerful strongly-typed theory is because there is just one model of the axioms of the theory up to a unique isomorphism, which formalizes the concept of "truth" that you mentioned in your post.
I looked up your papers... Then I noticed you have also worked on paraconsistent logic. So to just boldly go on a completely new tangent and ask a question I have long sought to ask: do you know a good introduction text for paraconsistent logic, for a graduate level computer science student?
> It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable."
If people want to understand how to reconcile this very vague statement with Goedel incompleteness theorem that appears to say that some "true" statements are in fact not provable, here's the rough idea: we distinguish between "theories", which live in syntactic world, and "models", which are meant to represent semantics. Theories are like specification of an interface of a programing module, and models are actual implementation of said modules. If one can implement an interface to satisfy all requirements of the specification (that is, all the axioms and theorem that the axioms entail), existence of such implementation shows that the specification is self-consistent: in math, we say that theories that have a model are consistent. What Goedel's completeness theorem says is the converse: consistent theories always have a model; in programming talk, non-contradictory specification can always be implemented.
Here's why it means that "all true things are provable": if something is supposed to be true fact about the theory, it has be a property of every model of said theory, that's the lowest bar for any notion of "truth" to make sense. But, one can easily show, using Goedel's completeness theorem, that if something is true in every model of the theory, it has to be provable: indeed, suppose that statement f is true in every model of theory T, but is actually not provable from T. We can then extend theory T by statement "not f", and the resulting theory T' = {T, "not f"} is still consistent, because for it to be inconsistent means exactly that T could prove both "not f" and "not (not f)", and the latter is equivalent f, which we assumed T cannot prove. Then, Goedel's completeness theorem says that this extended theory, since it's consistent, must have a model, M'. But, a model of this extend theory T' is also a model of basic theory T; if you implement larger specification, your implementation also implements any subset of it. But f was supposed to be true in every model of T, and so f is true in M', but also "not f" is true in M', which is a contradiction. Hence, f must be provable from T.
Why it doesn't conflict with Goedel's in-completeness theorem? After all, the Goedel's sentence constructed in the proof of Goedel's incompleteness theorem is supposed to express something true but not provable. Well, the idea is that it is not true of the theory of natural numbers, but it's true of the particular model of natural numbers that we have in mind when we think of what natural numbers are, the so called standard model of natural numbers, where all of the numbers are of the form 0 and, using OPs notation (next (next (next ... (next 0) ... )). As it turns out, there exist other models of natural numbers, which have extra, "non-standard" natural numbers which are not of that form, numbers you cannot reach by just applying successor operation finite number of times starting from 0. These models are really weird, but they still must abide all provable rules of the behavior of natural numbers. One can still add them, there must be some "prime" non-standard numbers that aren't products of any smaller numbers, the non-standard numbers must also split into unique product of prime numbers (some of which must necessarily also be non-standard), and so on. This is all crazy, and can make your mind twist, so only think about it at your own peril.
To sum up, the notion of "truth" with respect to theories coincides with provability, but not so when you start talking about things true in particular models. This means that we cannot describe all true things about specific models, and in particular about standard natural numbers, using standard logic, but if something does follow from the theory and is true in every of its models, it is in fact provable.
People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it to behave differently based on its own conclusion about its behavior.
What if I ask you to predict whether you’re going to go left or right, but I also tell you that I’m going to force you to go the opposite direction as what you predict? Then the set of things you can accurately predict is Incomplete. But that’s not a profound limitation of human consciousness, it’s just the familiar paradox of any fortune teller or time travel scenarios.
While this is true, it is surprising that is it impossible to engineer a system to be complete and consistent about arithmetic, as opposed to systems which are not engineered well, like your 2nd paragraph.
If I take "1 is even", "1 is odd" and "no number can be even and odd" as my axioms, then there is obviously a problem, but of my own doing.
Russel and Whitehead's system is well-engineered; that's why it doesn't prove a contradiction (presumably) while your badly engineered system does. The issue is that R&W made their system powerful enough that it's also incomplete, due to the fact that their system contains smartass statements like G that are hell-bent on creating paradoxes if given the chance.
Before Godel's time, people just didn't have enough experience with computers to realize that you have to deal with code injection attacks every time you try to build a powerful platform of any kind. In this case, Godel Numbering is the hack that allows code injection into a formal system that's supposed to just be highly insightful about properties of the infinite world of natural numbers.
Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".
> Because of the halting issue you cannot summarise reality into a set of axioms and rules
Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement...
Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Godel's proof is just an XSS attack on axiom systems whose designers think they're only "about numbers", like how CSS is designed to be about styling but it's also Turing-complete and vulnerable to XSS.
Russel and Whitehead were trying to simultaneously (1) invent a system capable of proving highly insightful claims about the infinite space of numbers, like "there doesn't exist a number between 1 and infinity with property P" but (2) not a system that can encode a Turing-equivalent agent that creates paradoxes if it tries to predict its own future.
Godel was just the first to point out that condition (2) was already met just by supporting Peano Arithmetic, the same way a modern computer science undergrad can point out that CSS is Turing-complete or your regex-based HTML validator is vulnerable to XSS attacks.
This is really excellent. Amazing how much clearer the author’s Lisp code makes things (even to a non mathematician and non lisper). It’s rare to find explanations of difficult topics that are this well communicated, but I hope it becomes a trend.
I agree and I want to add that I particularly appreciated how you consistently, in programming terms, communicated the type of things. Eg:
(proves a b)
So far saying “the sequence with the Gödel Number a proves the formula with Gödel Number b”
In my experience, most mathematicians would have instead written "So far saying 'a proves b'". Repeating the type of the parameters consistently made it significantly easier for me to follow along. I hope this becomes more common.
Something I've always been curious about: does Gödel's theorem imply an infinity of inconsistent statements, or is the "this statement cannot be proven..." statement the only one? If it's the latter, then of what practical significance is the singularity? If a system is incomplete only in that regard, couldn't one redefine incompleteness to exclude it, and render the system complete for all practical purposes?
Others have explained why you can't wave away inconsistency (principle of explosion) nor incompleteness (adding new axioms just creates a new axiomatic system with its own Godel sentences). However you might also find it interesting what incompletenesses exist in our own mathematical system (ZFC) -- the most well-known example is the Continuum Hypothesis[1]:
> There is no set whose cardinality is strictly between that of the integers and the real numbers.
Or to put it another way, there exists no intermediate type of infinity between countable infinities (the set of integers) and uncountable infinities (the set of real numbers).
The CH is independent of ZFC -- both CH and its negation can be included as new axioms to ZFC and both versions are logically consistent if and only if ZFC is -- meaning that being able to prove the CH is an incompleteness in ZFC.
> being able to prove the CH is an incompleteness in ZFC.
It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion.
But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and real numbers.
I thought that independent (undecidable) statements are totally different than the Gödel sentences which demonstrate incompleteness. The latter is a statement which is true in the axiomatic system but which cannot be proven using the axiomatic system. The former is just a statement that essentially has no truth value in the axiomatic system.
I think this partially answers your question: One thing people try to do to "fix" the incompleteness is to just add the Godel sentence as an axiom of the mathematical system. However, each time you do this, you can create yet another new Godel sentence for the new system with the new axiom. Since it's a diagonalization argument, no amount of adding of new axioms can permanently "fix" the system and make it complete -- there will always be new Godel sentence that is true but not provable.
> The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence.
Yes, but the "such as..." example incorporates the original "this statement is not provable" statement, so it seems a bit of a cheat. If you could exclude that statement, it would also by definition exclude any compound versions of it. It seems to me that the issue boils down to, can "this statement is not provable" be leveraged to get to something like 1 + 1 = 3?
Excellent question. It implies an infinite number of statements. For if T is such an incomplete theory and X is a statement true in some models of T and false in others, then T+X is also a theory that satisfies the same requirements as T in Godel's theorem. Therefore there is another statement Y that is true in some models of T+X and false in other models of T+X. But any model of T+X is a model of T so Y is true in some models of T and false in others. And it goes on...
It implies an infinity of inconsistent statements. I'm not a mathematician, but the way I understand it is to do an analogy with the halting problem: for any programming language that is powerful enough you can build a program where you don't know if it's going to halt or not.
About avoiding singularities, the GEB book (Godel,Escher,Bach) mentions at the beginning: mathematicians like Russel tried to avoid paradoxes by moving them out of the system, but Godel shown that it doesn't work if you want a complete and consistent system (complete and consistent are technical terms, Wikipedia does a good explanation: https://en.wikipedia.org/wiki/Kurt_Gödel#Incompleteness_theo...).
I think the question is a bit more specific in the context of the halting problem
We know by contradiction that we cannot write a program that determines if any program halts, if the program being checked also contains the program that determines if itself halts.
Is this the only class of program that cannot be determined to halt?
if P is (this statement cannot be proved), then you can't prove A && P for any provable A, either. There's an infinite number of statements that can be proven (1=1, 2=2, 3=3... for starters) so there's an infinite number of statements that can't be proven.
There are less trivial classes of statements that can't be proven. For instance, there's an infinite number of statements like "bit N of Chaitin's constant is 1" that cannot be proven (only a finite number of those statements are provable).
There are an infinitely many propositions that cannot be proved
or disproved in foundational theories of Computer Science.
However, foundational theories exclude the [Gödel 1831]
proposition *I'mUnprovable* because including it would
make the theories inconsistent for reasons mentioned
elsewhere in this discussion.
So if we have a theory expressive enough to make statements about ordinary (Peano) arithmetic, we can always form a self-referential statement within the framework of this theory which we can not prove or disprove. So far, so good. Here is my question: What happens if we restrict/weaken the theory to preclude self-referential statements? Obviously, we will lose our ability to express certain arithmetic statements which correspond to self-referential statements in the original theory. But what else? Is that the only class of statements we lose? Also, are there any other kinds of statements that still make the theory incomplete?
It is very hard to detect self-referential statements and restricting yourself to "non-self-referential statements" might be quite severe.
Given a set of "domino" tiles - each having a top and a bottom. Each top and bottom has some word on it - these words can only use the letters "a" and "b".
You can duplicate domino tiles and also align tiles so that all tops and all bottoms are aligned.
Now, given a finite set of such tiles, can you say whether there is an alignment so that all tops concatenated, read from right to left, equal all bottoms concatenated?
In fact, given such a set of tiles S, you can easily create a formula P(S) that is true iff such a valid alignment does not exist. Obviously this formula is true for some sets of tiles and false for others.
Now the funny thing: Given a (correct) fixed theory T in which you can state P(S) for every S and in which proofs can be computationally checked, there must be infinitely many S so that P(S) is true, but cannot be proved in T. Thus such theory T is incomplete.
Where is the self-reference?
This problem is also known as the Post correspondence problem (PCP). The halting problem can be reduced to it, which is not decidable. If T was complete, you could enumerating all proofs and see whether they correctly proof P(S) or its negation. Due to its completeness you would eventually find a proof for either of them and thus you could decide the halting problem.
We lose the ability to reason about sets of unbounded size. As long as we only restrict ourselves to some bounded subset of integers, Gödel can't do the trick with his numerals. Equivalently, on the CS side, we must restrict ourselves to total functions, that is, all valid programs must provably halt after some bounded number of steps.
Contrary to popular opinion, [Gödel 1931] did not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the reasons explained here:
I really like the conversion to a representation that's more familiar but I suspect it's also confusing me. Here are the questions that I have to start:
Does 'there-is' evaluate to a boolean (is boolean a thing? is evaluation a thing?)
I was surprised that the axioms don't use there-is but I sense I shouldn't be?
what does '(when 0 (or 0 1))' mean, it's described as 'when 0, then there is either 0 or 1' but I'm not sure what that means? is '(when 0 0)' true and '(when 1 0)' false? Why not use '(when A B)' as equals?
Not a question but in the axioms I assume pairs should be pears and applies should be apples.
How goes 'implies' get introduced by '(when (when q r) (when (or p q) (or p r))'? Also, this introduces a category in the example i.e. fruits but not sure how that happened.
Why do we need to have second '(not (factor? x 3^22 ...))', isn't it sufficient to say that (factor? x 3^21 ...) to establish that the 2nd term is 'there-is'?
For existential quantification, we use the `there-is` function.
Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification.
Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.
I took these to mean the existential operator and the implication operator, but I agree they were insufficiently defined for me, esp. as we're building from first principles. The post could have made the early proofs more obvious in how they were constructed (e.g. how the language is really used to prove statements).
Readit News
Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason:
Furthermore, existence of the proposition I'mUnprovable contradicts the following fundamental theorem of provability that goes all the way back to Euclid: See the following article for further details:https://papers.ssrn.com/abstract=3603021
https://en.wikipedia.org/wiki/Carl_Hewitt
Deleted Comment
I point it out only because your work here is so good that it feels wrong not to smooth out any small splinters.
Thank you for making this!
1. Please don't bring the notion of truth into an introductory explanation (such as in the section "Power of Numbers" or in the short intro to "Hilbert's Program"). It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable." Just stick to incompleteness and consistency at a syntactic level instead of appealing to truth, that is respectively the ability to always add new axioms and the lack of syntactic contradictions.
2. The lack of a system S's ability to prove its own consistency is not interesting by itself since we would not trust a proof from a potentially inconsistent system. Hence it is not, in a sense, terribly interesting that we require an infinite tower of increasingly stronger systems to prove the consistency of S and themselves. Rather the interesting direction goes the other way. S cannot prove the consistency of stronger systems, which means we cannot have a "minimal" system we use to explore the consistency of all other systems (again subject to some nuance).
Sorry for the confusion. We detach comments that are replies to the top comment but don't respond to anything specific that that comment said. This is standard moderation. Sometimes we post that we did this (https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...), but not always.
We do this because users often post replies to the top comment on a page that aren't really replies. Sometimes they do that because they want to get their comment higher on the page (so-called topjacking). Of course that's not always the case.
Both of your posts are fine (except for the fact that they duplicate one another) but they are replies to the article, not to anything that the top comment (https://news.ycombinator.com/item?id=25116881) specifically says. Indeed your sentence "I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap." makes it quite clear that your reply is to the article, not xyzzyz's comment. That's great! But the appropriate level for such a comment is the top level of the thread.
I've therefore done the same again and detached this subthread from https://news.ycombinator.com/item?id=25116881.
--
Poking through your history, why do you quibble on the word truth so often? Do we not agree there are statements that are true? Do we not agree there are provable true statements ? If there are unprovable statements in any consistent set of axioms, might we also conclude there also be an unprovable but true statements?
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?).
To offer possibly a comment to yours about the notion of "truth", in the article posted, when I read "true" (e.g. in the 1st paragraph of chapter Hilbert's Program) and next to it "false", I immediately made reference in my mind to the true/false duality of programmers. I think that helped in understanding the article, but coupled with a footnote with your details would certainly help the reader think further on the topic.
cheers :-)
mathematics of computer science. The axioms of powerful
foundational theories of computer science have just one model
up to a unique isomorphism. See
https://papers.ssrn.com/abstract=3418003 and https://papers.ssrn.com/abstract=3457802
Actually, powerful strongly-typed theories used in Computer Science can prove their own consistency!
See the following article for for how this is done:
https://papers.ssrn.com/abstract=3603021
As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference.
Instead our confidence in the consistency of a powerful strongly-typed theory is because there is just one model of the axioms of the theory up to a unique isomorphism, which formalizes the concept of "truth" that you mentioned in your post.
For example, see the following article:
https://papers.ssrn.com/abstract=3457802
If people want to understand how to reconcile this very vague statement with Goedel incompleteness theorem that appears to say that some "true" statements are in fact not provable, here's the rough idea: we distinguish between "theories", which live in syntactic world, and "models", which are meant to represent semantics. Theories are like specification of an interface of a programing module, and models are actual implementation of said modules. If one can implement an interface to satisfy all requirements of the specification (that is, all the axioms and theorem that the axioms entail), existence of such implementation shows that the specification is self-consistent: in math, we say that theories that have a model are consistent. What Goedel's completeness theorem says is the converse: consistent theories always have a model; in programming talk, non-contradictory specification can always be implemented.
Here's why it means that "all true things are provable": if something is supposed to be true fact about the theory, it has be a property of every model of said theory, that's the lowest bar for any notion of "truth" to make sense. But, one can easily show, using Goedel's completeness theorem, that if something is true in every model of the theory, it has to be provable: indeed, suppose that statement f is true in every model of theory T, but is actually not provable from T. We can then extend theory T by statement "not f", and the resulting theory T' = {T, "not f"} is still consistent, because for it to be inconsistent means exactly that T could prove both "not f" and "not (not f)", and the latter is equivalent f, which we assumed T cannot prove. Then, Goedel's completeness theorem says that this extended theory, since it's consistent, must have a model, M'. But, a model of this extend theory T' is also a model of basic theory T; if you implement larger specification, your implementation also implements any subset of it. But f was supposed to be true in every model of T, and so f is true in M', but also "not f" is true in M', which is a contradiction. Hence, f must be provable from T.
Why it doesn't conflict with Goedel's in-completeness theorem? After all, the Goedel's sentence constructed in the proof of Goedel's incompleteness theorem is supposed to express something true but not provable. Well, the idea is that it is not true of the theory of natural numbers, but it's true of the particular model of natural numbers that we have in mind when we think of what natural numbers are, the so called standard model of natural numbers, where all of the numbers are of the form 0 and, using OPs notation (next (next (next ... (next 0) ... )). As it turns out, there exist other models of natural numbers, which have extra, "non-standard" natural numbers which are not of that form, numbers you cannot reach by just applying successor operation finite number of times starting from 0. These models are really weird, but they still must abide all provable rules of the behavior of natural numbers. One can still add them, there must be some "prime" non-standard numbers that aren't products of any smaller numbers, the non-standard numbers must also split into unique product of prime numbers (some of which must necessarily also be non-standard), and so on. This is all crazy, and can make your mind twist, so only think about it at your own peril.
To sum up, the notion of "truth" with respect to theories coincides with provability, but not so when you start talking about things true in particular models. This means that we cannot describe all true things about specific models, and in particular about standard natural numbers, using standard logic, but if something does follow from the theory and is true in every of its models, it is in fact provable.
Goedel incompleteness theorem -> apply this to "theories"
Goedel completeness theorem -> apply this to a specific "model", of the theory
So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?
What if I ask you to predict whether you’re going to go left or right, but I also tell you that I’m going to force you to go the opposite direction as what you predict? Then the set of things you can accurately predict is Incomplete. But that’s not a profound limitation of human consciousness, it’s just the familiar paradox of any fortune teller or time travel scenarios.
If I take "1 is even", "1 is odd" and "no number can be even and odd" as my axioms, then there is obviously a problem, but of my own doing.
Before Godel's time, people just didn't have enough experience with computers to realize that you have to deal with code injection attacks every time you try to build a powerful platform of any kind. In this case, Godel Numbering is the hack that allows code injection into a formal system that's supposed to just be highly insightful about properties of the infinite world of natural numbers.
Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement...
Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Godel's proof is just an XSS attack on axiom systems whose designers think they're only "about numbers", like how CSS is designed to be about styling but it's also Turing-complete and vulnerable to XSS.
Russel and Whitehead were trying to simultaneously (1) invent a system capable of proving highly insightful claims about the infinite space of numbers, like "there doesn't exist a number between 1 and infinity with property P" but (2) not a system that can encode a Turing-equivalent agent that creates paradoxes if it tries to predict its own future.
Godel was just the first to point out that condition (2) was already met just by supporting Peano Arithmetic, the same way a modern computer science undergrad can point out that CSS is Turing-complete or your regex-based HTML validator is vulnerable to XSS attacks.
The predicate Halt<aType>[anExpression] is true if and only
if anExpression of type aType halts.
The predicate Halt is inferentially undecidable, that is, it
is not the case that for every expression anExpression of type aType that
|- Halt<aType>[anExpression] or |- ~Halt<aType>[anExpression].
Inferential undecidability does not mean that mathematics
is wrong.
Of course, it is possible to have incorrect
mathematical proofs, such as the incorrect proof in
[Gödel 1931] for the inferential undecidability of Russell's
Principia Mathematica. (There is a correct proof here:
https://papers.ssrn.com/abstract=3603021)
Your intuition is pretty good.
A correct proof of inferential incompleteness of Russell's
Principia Mathematica can be constructed using the
computational undecidability of the halting problem.
See https://papers.ssrn.com/abstract=3603021
In my experience, most mathematicians would have instead written "So far saying 'a proves b'". Repeating the type of the parameters consistently made it significantly easier for me to follow along. I hope this becomes more common.
> There is no set whose cardinality is strictly between that of the integers and the real numbers.
Or to put it another way, there exists no intermediate type of infinity between countable infinities (the set of integers) and uncountable infinities (the set of real numbers).
The CH is independent of ZFC -- both CH and its negation can be included as new axioms to ZFC and both versions are logically consistent if and only if ZFC is -- meaning that being able to prove the CH is an incompleteness in ZFC.
[1]: https://en.wikipedia.org/wiki/Continuum_hypothesis
It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion.
But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and real numbers.
https://www.scottaaronson.com/blog/?p=4974
And (of course) the HN discussion at the time:
https://news.ycombinator.com/item?id=24954695
https://papers.ssrn.com/abstract=3457802, which is much
more powerful
than first-order ZFC), one version ofthe Continuum Hypothesis is still open although other
versions have been proved or disproved.
> The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence.
[0] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
About avoiding singularities, the GEB book (Godel,Escher,Bach) mentions at the beginning: mathematicians like Russel tried to avoid paradoxes by moving them out of the system, but Godel shown that it doesn't work if you want a complete and consistent system (complete and consistent are technical terms, Wikipedia does a good explanation: https://en.wikipedia.org/wiki/Kurt_Gödel#Incompleteness_theo...).
Also related to your question: https://en.wikipedia.org/wiki/Chaitin%27s_constant
Sorry if I don't get the technical terms right, hopefully someone else in HN can explain this better.
We know by contradiction that we cannot write a program that determines if any program halts, if the program being checked also contains the program that determines if itself halts.
Is this the only class of program that cannot be determined to halt?
There are less trivial classes of statements that can't be proven. For instance, there's an infinite number of statements like "bit N of Chaitin's constant is 1" that cannot be proven (only a finite number of those statements are provable).
https://en.wikipedia.org/wiki/Chaitin%27s_constant#Incomplet...
or disproved in foundational theories of Computer Science.
Given a set of "domino" tiles - each having a top and a bottom. Each top and bottom has some word on it - these words can only use the letters "a" and "b". You can duplicate domino tiles and also align tiles so that all tops and all bottoms are aligned.
Now, given a finite set of such tiles, can you say whether there is an alignment so that all tops concatenated, read from right to left, equal all bottoms concatenated?
In fact, given such a set of tiles S, you can easily create a formula P(S) that is true iff such a valid alignment does not exist. Obviously this formula is true for some sets of tiles and false for others.
Now the funny thing: Given a (correct) fixed theory T in which you can state P(S) for every S and in which proofs can be computationally checked, there must be infinitely many S so that P(S) is true, but cannot be proved in T. Thus such theory T is incomplete.
Where is the self-reference?
This problem is also known as the Post correspondence problem (PCP). The halting problem can be reduced to it, which is not decidable. If T was complete, you could enumerating all proofs and see whether they correctly proof P(S) or its negation. Due to its completeness you would eventually find a proof for either of them and thus you could decide the halting problem.
Mathematical already excludes construction of the [Gödel 1931]
proposition I'mUnprovable because of orders on propositions.
https://papers.ssrn.com/abstract=3603021
The article linked above gives a correct proof of inferential incompleteness.
Does 'there-is' evaluate to a boolean (is boolean a thing? is evaluation a thing?)
I was surprised that the axioms don't use there-is but I sense I shouldn't be?
what does '(when 0 (or 0 1))' mean, it's described as 'when 0, then there is either 0 or 1' but I'm not sure what that means? is '(when 0 0)' true and '(when 1 0)' false? Why not use '(when A B)' as equals?
Not a question but in the axioms I assume pairs should be pears and applies should be apples.
How goes 'implies' get introduced by '(when (when q r) (when (or p q) (or p r))'? Also, this introduces a category in the example i.e. fruits but not sure how that happened.
Why do we need to have second '(not (factor? x 3^22 ...))', isn't it sufficient to say that (factor? x 3^21 ...) to establish that the 2nd term is 'there-is'?
Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification.
Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.