> 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.
As you said, we tend to call the statement "true" because we know that the formal system itself was designed with the intention to describe natural numbers and arithmetic, and the statement was designed intentionally to refer indirectly to itself and claim its own unprovability. Since the statement is formally unprovable, we interpret it as being true. I had forgotten that Gödel actually showed that there are other interpretations of the formal system in which the Gödel statement is false.
The Godel sentences are of a different character than the continuum hypothesis (CH) because the Godel sentences are simple first-order arithmetic statements, while the CH is a higher-order, a.k.a. analytic statement. A Godel sentence can be assigned a truth meaning via Tarski's definition of truth independent of the axiom system in a way that is much harder to do with the CH.
Basically a Godel sentence says something about whether a given piece of software terminates when run on an ideal computer (specifically a piece of software that hunts for a proof of a contradiction within a specified axiom system). I'll argue that whether a specific piece of software would halt or not when run on an ideal machine has a definite truth value independent of any axiom system. Whereas CH doesn't really afford such a software interpretation.
I do respect the fact that there exist models of PA + ~Con(PA) but these models are non-standard and we don't use such models to reason about software, specifically because they are unsound in this sense.
But as others have said, both statements are equally unprovable in ZFC. The Godel sentences demonstrating incompleteness are constructed in such a way that you could argue (outside of the axiomatic system) they are provably true or false, while CH is a case where reasonable mathematicians may disagree on whether it is true or false. But ultimately there is no proof in ZFC for either, so they are both examples of incompleteness in ZFC.
And note that the Godel sentence demonstrating incompleteness doesn't need to be true -- the inverse of the Godel sentence demonstrating incompleteness is also unprovable.
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.
The CH is a syntactically valid statement in ZFC.
So, shouldn't the fact that ZFC cannot prove or disprove CH, be an example of ZFC being incomplete, regardless of whether CH is in fact true, false, or not-a-proposition-that-has-a-truth-value ?
Here's a good list: https://en.wikipedia.org/wiki/Completeness_(logic)#Forms_of_...
The existence of a proof within the logic system for every well-formed formula or its negation is "syntactical completeness".
CH is independent of ZFC, period, as proved by Cohen. Talking about 'semantic level' does not make sense.
CH is an example of the incompleteness of ZFC. There are models of ZFC in which CH is true and models in which CH is false.
For specific example, what is a model of ZFC? Is it just another theory, one which includes ZFC and few more axioms? Why not call it a derived theory or a subset theory?
It's much easier to understand if we take an example. An example of a theory is the single sentence:
"There exists an X and there exists a Y such that X is not equal to Y."
(Of course typically in logic you would use logic symbols, but here I am writing out in an English sentence.)
Now, a model of this theory is the set {1,2}. Another model is the set {1,2,3}. More generally: any set with at least two elements is a model of that theory. The "function symbols" and "relation symbols" can be introduced in the language to talk about operations like addition and multiplication.
For example, the theory of groups uses the language of groups with a binary function symbol representing group multiplication. Any group (such as the integers with addition or invertible matrices with matrix multiplication) is a model of that theory.
So: theories are sets of axioms in some language, and models are sets together with actual functions/relations that satisfy those axioms.
Models of ZFC are a little bit counterintuitive. But they are single sets that interpret all the axioms of ZFC, rather than actual sets that we use in informal mathematics. Models of ZFC can be quite unusual because of the incompleteness theorem, and there are infinitely many models because of this (such as some in which CH is true, etc.).
https://www.scottaaronson.com/blog/?p=4974
And (of course) the HN discussion at the time:
https://papers.ssrn.com/abstract=3457802, which is much
more powerful than first-order ZFC), one version of
the Continuum Hypothesis is still open although other
versions have been proved or disproved.
It has *not* been proved that the open version cannot be
proved and it has *not* been proved that the open
version cannot be 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_...
What Gödel did prove was that the above list of statements (and infinitely more) must exist.
The special thing about his proof is indeed that it is recursive, i.e. adding another axiom can't fix the problem. But that was only necessary to prove that no formal system can be perfect, ever.
Most undecidable problems can indeed be "fixed" by adding another axiom, but if you go beyond the ones of ZFC it becomes less clear which of the two alternatives is the "right" one...
But "this statement is not provable" isn't a statement in the logic. It's an English language description of a type of statement, one which has certain self-referential characteristics and shows us the incompleteness of the logic.
There are an infinite number of statements in the logic which fit that type by having the relevant characteristics, and they aren't all obvious. The self-referential recursion implied in Gödel's construction is designed to make it obvious, but it can be encoded in less and less obvious ways while still containing an encoded image of themselves.
You can even get to statements where the self-reference is encrypted (using an actual encryption algorithm)! Only a mathematician with the "secret key", or a clever super-mathematician with amazing brute-forcing skills, would be able to read the statement and confirm that it's true!
And so "perceivable truth" is a thing too. Some truths are too complex for an ordinary mind to verify, yet still true.
To exclude all self-referential statements in the logic of type "this statement is not provable", you would need a decision procedure to tell you which statements in the logic are those.
Unfortunately you can't make such a decision procedure. It's very similar to Turing's halting problem. Just as you can't make a program which will take any input X and tell you if the program encoded as X will eventually terminate, you can't make a procedure which will take any statement S and tell you if it contains a fancy encoding of itself.
There's just no way to do it. The fact it can be related to Turing's halting problem, which is about real machines and real algorithms running on them, may give you some idea that the core principle can be grounded in something quite down to earth which affects practical applications.
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?
All undecidable languages that are recognizable in some sense contain a self referential program sneaking within it. This is because the halting problem is complete for its complexity class and hence any undecidable but recognizable language is Turing reducible to the halting problem.
However for undecidable and unrecognizable languages, there are proofs of undecidability that are independent of diagonalization and instead use other proof techniques that in a very strong sense are entirely independent of self-reference. Of course this isn't a formal answer mostly because the idea of a self referential program is not a formal concept but there are techniques such as reverse mathematics [1] that can be used to determine a minimal set of axioms needed to prove a theorem along with proof techniques that depend on the Low basis theorem [2] that are able to prove that some languages are undecidable and unrecognizable that do not in any way depend on diagonalization, which is the proof technique that is associated with self referential programs.
Can you tell if the program halts? You can’t without proving the conjeture.
Also, a lot of problems are proven unsolvable because solving them would imply solving the halting problem, but hey.
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.
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.