5 ms·

Others have explained why you can't wave away inconsistency (principle of explosion) nor incompleteness (adding new axioms just creates a new axiomatic system w

by cyphar 6y ago

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. [1]: https://en.wikipedia.org/wiki/Continuum_hypothesis https://en.wikipedia.org/wiki/Continuum_hypothesis

tshaddox 6y ago
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.
- deleted 6y ago
  [deleted]
- a1369209993 6y ago
  Something being true in a axiomatic system is the same thing as it being provable; that's what "true" means. While a Godel statement for X can be interpreted as "X does not prove this statement", that interpretation inherently relies on the semantic implied by X. The Godel construction is systematic way of generating independent statements without needing to know anything specific about the axiomatic system.
  - tshaddox 6y ago
    Ah yes, you're right, and my lazy wording in the former comment is inaccurate. A Gödel sentence is just a statement written in the syntax of whatever formal system we're dealing with: generally, it's a statement that there exists no natural number which satisfies a particular property. The formal system cannot prove or disprove that statement. 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.
- deleted 6y ago
  [deleted]
- rssoconnor 6y ago
  Your thoughts are approximately correct. 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.
- cyphar 6y ago
  You're quite right that CH is not an example of a Godel sentence which demonstrates incompleteness (examples of that are given in the linked article) -- I didn't mean to imply otherwise. I just wanted to share that this was a more practical example of incompleteness in our modern mathematical framework (ZFC) which folks might find interesting. 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.
jlokier 6y ago
> 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.
- deleted 6y ago
  [deleted]
- drdeca 6y ago
  Hm? I thought (in)completeness was just about whether or not , for each well-formed-formula, either there is a proof of it, or a proof of its negation. 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 ?
  - jlokier 6y ago
    Ok. If we are being careful, there are different kinds of completeness and we should specify which one we're talking about. Here's a good list: https://en.wikipedia.org/wiki/Completeness_(logic)#Forms_of_completeness 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".
    - drdeca 6y ago
      Oh cool, I was (at least partially) wrong. (Or, I was missing something important at least.) I appreciate the correction/elaboration.
- deleted 6y ago
  [deleted]
- redvenom 6y ago
kkylin 6y ago
For anyone interested in the consistency of CH and Axiom of Choice: https://www.scottaaronson.com/blog/?p=4974 https://www.scottaaronson.com/blog/?p=4974 And (of course) the HN discussion at the time: https://news.ycombinator.com/item?id=24954695 https://news.ycombinator.com/item?id=24954695
ProfHewitt 6y ago
In foundational theories that are strongly typed (such as https://papers.ssrn.com/abstract=3457802 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.

by cyphar 6y ago

tshaddox 6y ago

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.

deleted 6y ago
[deleted]
a1369209993 6y ago
Something being true in a axiomatic system is the same thing as it being provable; that's what "true" means. While a Godel statement for X can be interpreted as "X does not prove this statement", that interpretation inherently relies on the semantic implied by X. The Godel construction is systematic way of generating independent statements without needing to know anything specific about the axiomatic system.
- tshaddox 6y ago
  Ah yes, you're right, and my lazy wording in the former comment is inaccurate. A Gödel sentence is just a statement written in the syntax of whatever formal system we're dealing with: generally, it's a statement that there exists no natural number which satisfies a particular property. The formal system cannot prove or disprove that statement. 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.
deleted 6y ago
[deleted]
rssoconnor 6y ago
Your thoughts are approximately correct. 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.
cyphar 6y ago
You're quite right that CH is not an example of a Godel sentence which demonstrates incompleteness (examples of that are given in the linked article) -- I didn't mean to imply otherwise. I just wanted to share that this was a more practical example of incompleteness in our modern mathematical framework (ZFC) which folks might find interesting. 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.

jlokier 6y ago

> 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.

deleted 6y ago
[deleted]
drdeca 6y ago
Hm? I thought (in)completeness was just about whether or not , for each well-formed-formula, either there is a proof of it, or a proof of its negation. 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 ?
- jlokier 6y ago
  Ok. If we are being careful, there are different kinds of completeness and we should specify which one we're talking about. Here's a good list: https://en.wikipedia.org/wiki/Completeness_(logic)#Forms_of_completeness 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".
  - drdeca 6y ago
    Oh cool, I was (at least partially) wrong. (Or, I was missing something important at least.) I appreciate the correction/elaboration.
deleted 6y ago
[deleted]
redvenom 6y ago

kkylin 6y ago

For anyone interested in the consistency of CH and Axiom of Choice: https://www.scottaaronson.com/blog/?p=4974 https://www.scottaaronson.com/blog/?p=4974 And (of course) the HN discussion at the time: https://news.ycombinator.com/item?id=24954695 https://news.ycombinator.com/item?id=24954695

ProfHewitt 6y ago

In foundational theories that are strongly typed (such as https://papers.ssrn.com/abstract=3457802 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.