5 ms·

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symboli

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable. This is an often repeated claim, but I can’t shake the feeling that it’s an incorrectly drawn conclusion (of Gödel’s incompleteness theorems). My understanding: It’s true that there are such “mathematical truths without proofs within axiomatic system X”, but they are unreachable by mathematicians and symbolic logic / machines alike. If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. Please correct me if I’m wrong.

simias 5y ago
>If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. I mean in the end Godel's own proof effectively relies on this: he builds a proposition using the rule of the system saying "this proposition has no proof" and at this point you either have to accept that the proposition is incorrect, but then your system is inconsistent (it can be used to derive falsehoods) or that it is correct but then the system is incomplete. So you may decide not to call it a truth but you also can't really call it a falsehood. I would also wager that mathematicians generally prefer incomplete to inconsistent systems, if which case you have to accept that these unprovable propositions are indeed truths. It's like the "does the set of all sets not containing themselves contain itself" paradox, you can't just ignore it as irrelevant because it puts into question your entire formal system.
- Filligree 5y ago
  > I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. Is that true? It seems to me that if a statement is unprovable, then even if it would in theory render your system inconsistent, there's no way that can actually happen. Since, if you found any example of a chain of logic which leads to an inconsistency, that would count as a proof of the original statement. Which is unprovable, and as such can't have proofs.
  - simias 5y ago
    But what if the statement is "this statement can't be proven"? You haven't proven the statement, you've proven that it can't be proven. See https://youtu.be/HeQX2HjkcNo?t=926 https://youtu.be/HeQX2HjkcNo?t=926 for instance which is (IMO) a fairly good explanation of the proof and why you end up with something both true and not provable. Penrose's "Emperor's New Mind" also discusses this topic at length (within the context of whether human brains can be emulated). I wasn't convinced with his argument regarding AI but his overview of the problem of what's computable and what's not is rather good if a bit dense.
    - Filligree 5y ago
      > Penrose's "Emperor's New Mind" also discusses this topic at length (within the context of whether human brains can be emulated). I wasn't convinced with his argument regarding AI but his overview of the problem of what's computable and what's not is rather good if a bit dense. As far as I'm aware physics is computable, so I don't buy that one. :) At most one might argue that there are high-level optimizations to be had, which can't be used because they're uncomputable. In which case is it really an optimization?
      - simias 5y ago
        That's part of his arguments, that some corners of quantum physics that still elude us (quantum gravity and all that) may be undecidable. He then goes on to explain how he thinks these phenomena could have an influence on cognition. I don't really buy this theory, but the book is basically 80% "here's what we know" and 20% "here's what I conjecture" so it's still a worthwhile read IMO. It's worth noting that it's a book from the late 80's however, so it's a bit outdated in some parts (he didn't know that the universe's expansion was accelerating in particular, which renders his discussion of the curvature of the universe a bit obsolete).
  - ProfHewitt 5y ago
    It turns out that foundational mathematical systems can prove their own consistency. See the following: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, the proof is not convincing because the proof is valid even if the system is inconsistent!
garmaine 5y ago
I believe it is correct to say there are undecidable theorems in some limited type systems which cannot be proven, but which can be once you extend the type system (e.g. by making it higher-level or dependent). So in those limited systems we know there are things that are "true" or "false", but which can only be proven when we have a superset of the original tools available. And by extension, maybe in our more complete type system there are things which can't be proven yet, but could perhaps be if there were better tools available? Maybe another angle to look at it: one of the things which is difficult to prove is the halting problem. Maybe you can't prove that a given program will terminate. But you could run that program and watch it terminate, and then you'd know it does. In that sense there is a "true" answer, but one which couldn't have been proved in advance from type theory. But I admit I only have a high-level understanding of these things. Type theory and axiomatic mathematics is something I'd like to know more about.
UncleMeat 5y ago
> If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. This depends on your formalism for logic. Intuitionist logic merges the meaning of "true" and "has a proof" but classical logic does not have any problem with having a thing be called "true" while also not being provable.
rocqua 5y ago
I believe most constructive mathematics (mathematics not using the law of the exluded middle) is actually weaker than peano arithmetic. Certainly there is less that has been proven in it. Most type theory is constructive afaik, hence it might be weaker than even Godel implies.
- zozbot234 5y ago
  Constructive mathematics can prove anything that classical mathematics can, and more. The only catch is that propositions which are proven classically must always be stated in the negative fragment of the logic: there's no general duality as there is in classical logic, but a positive and a negative statement mean something different.
  - Koshkin 5y ago
    > and more I am not sure about that - there are some "pathological" phenomena in classical math that are rejected (for the lack of proof) in constructive math.
    - deleted 5y ago
      [deleted]
  - rocqua 5y ago
    How does this work for the banach tarski paradox?
    - zozbot234 5y ago
      That depends on the axiom of choice. From a constructive POV, this means you would have to introduce some sort of extra assumptions to the theorem itself. (The axiom of choice is also inconsistent with some popular extensions to constructive mathematics, so Banach-Tarski simply cannot apply to those mathematical objects.)
auggierose 5y ago
ZFC comes with First-Order Logic and is certainly complete. You are right in that sense. Let me be more specific: Given a sentence that is true in every model of ZFC, you can prove that sentence. This is true because ZFC is a first-order theory, and this is a property of ANY first-order theory. People that are pointing out incompleteness are talking about something else: They are talking about the fact that there are sentences S where neither S nor not S is provable. Additionally, there is a meta reason why S is believed to be true. For example, take S = encoding of "ZFC is consistent". BUT: This sentence S is true in some models of ZFC, and false in others, because otherwise the completeness of ZFC would make it provable / disprovable. So this boils down to the meta-truth being different from truth in a model. Disclaimer: I just recently looked seriously into this stuff, because I was wondering about completeness of a logic I invented. So if the above is wrong, please somebody correct me!
rssoconnor 5y ago
There are true (in the sense of Tarski's definition of truth) but unprovable (Π₁) sentences in any consistent (sufficiently powerful) system. Which of these true sentences are unprovable varies from system to system. Π₁-sentences (see arithmetical hierarchy) are closed formulas of the form, ∀x:ℕ. P(x), where P is some decidable predicate. i.e. all quantifiers in P are bounded. Thus for any given fixed value for x, say n, P(n) can be expanded out into conjunctions and disjunctions of atomic equalities and inequalities between closed arithmetic formula and those (in)equalities can in turn be decided (in principle) by calculation. Notice that 'x' is a formal variable in the language of first order logic, while we are using 'n' as a meta-variable denoting a term representing a numeral, e.g. 42. Σ₁-sentences are closed formulas of the form, ∃x:ℕ. P(x), where P is again a decidable predicate. Some basic first order logic yields that the negation of a Σ₁-sentence is logically equivalent to a Π₁-sentences and similarly the negation of a Π₁-sentence is logically equivalent to a Σ₁-sentence. Important Fact: All true Σ₁-sentences are provable (in any sufficiently powerful system). Why? Suppose ∃x. P(x) is true. Then, there is some numeral 'n' where P(n) is true. Since P(n) is decidable we can prove P(n) when P(n) is true. And, by the rule of existential introduction, ∃x.P(x) is provable from P(n). Now, let us consider some consistent system T (which is "sufficiently powerful"). For example, we can take T to be ZFC if you think ZFC is consistent. We can construct a Goedel-Rosser sentence for T, let's call this sentence G. G is a Π₁-sentence by construction, so we can put G in the form of ∀x:ℕ. P(x) for some decidable predicate P. Now either G is true, (i.e. ∀x:ℕ. P(x) is true) or ¬G is true, (i.e. ∃x:ℕ. ¬P(x) is true). Suppose ¬G is true. Since ¬G is (equivalent to) a Σ₁-sentence then T proves ¬G. But by the Goedel-Rosser incompleteness theorem, this would imply that T is inconsistent, contradicting our assumption. Thus it must be the case that G is true. However G is unprovable in T because, again by the Goedel-Rosser incompleteness theorem, if G were provable in T, then T would be inconsistent, contradicting our assumption. Thus G is an example of a true sentence that isn't provable in T.
- ProfHewitt 5y ago
  The halting problem provides examples of true but unprovable propositions because there are some expressions that do not halt but it is unprovable that they do not halt.
- 5y ago

simias 5y ago

>If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. I mean in the end Godel's own proof effectively relies on this: he builds a proposition using the rule of the system saying "this proposition has no proof" and at this point you either have to accept that the proposition is incorrect, but then your system is inconsistent (it can be used to derive falsehoods) or that it is correct but then the system is incomplete. So you may decide not to call it a truth but you also can't really call it a falsehood. I would also wager that mathematicians generally prefer incomplete to inconsistent systems, if which case you have to accept that these unprovable propositions are indeed truths. It's like the "does the set of all sets not containing themselves contain itself" paradox, you can't just ignore it as irrelevant because it puts into question your entire formal system.

Filligree 5y ago
> I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. Is that true? It seems to me that if a statement is unprovable, then even if it would in theory render your system inconsistent, there's no way that can actually happen. Since, if you found any example of a chain of logic which leads to an inconsistency, that would count as a proof of the original statement. Which is unprovable, and as such can't have proofs.
- simias 5y ago
  But what if the statement is "this statement can't be proven"? You haven't proven the statement, you've proven that it can't be proven. See https://youtu.be/HeQX2HjkcNo?t=926 https://youtu.be/HeQX2HjkcNo?t=926 for instance which is (IMO) a fairly good explanation of the proof and why you end up with something both true and not provable. Penrose's "Emperor's New Mind" also discusses this topic at length (within the context of whether human brains can be emulated). I wasn't convinced with his argument regarding AI but his overview of the problem of what's computable and what's not is rather good if a bit dense.
  - Filligree 5y ago
    > Penrose's "Emperor's New Mind" also discusses this topic at length (within the context of whether human brains can be emulated). I wasn't convinced with his argument regarding AI but his overview of the problem of what's computable and what's not is rather good if a bit dense. As far as I'm aware physics is computable, so I don't buy that one. :) At most one might argue that there are high-level optimizations to be had, which can't be used because they're uncomputable. In which case is it really an optimization?
    - simias 5y ago
      That's part of his arguments, that some corners of quantum physics that still elude us (quantum gravity and all that) may be undecidable. He then goes on to explain how he thinks these phenomena could have an influence on cognition. I don't really buy this theory, but the book is basically 80% "here's what we know" and 20% "here's what I conjecture" so it's still a worthwhile read IMO. It's worth noting that it's a book from the late 80's however, so it's a bit outdated in some parts (he didn't know that the universe's expansion was accelerating in particular, which renders his discussion of the curvature of the universe a bit obsolete).
- ProfHewitt 5y ago
  It turns out that foundational mathematical systems can prove their own consistency. See the following: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, the proof is not convincing because the proof is valid even if the system is inconsistent!

garmaine 5y ago

I believe it is correct to say there are undecidable theorems in some limited type systems which cannot be proven, but which can be once you extend the type system (e.g. by making it higher-level or dependent). So in those limited systems we know there are things that are "true" or "false", but which can only be proven when we have a superset of the original tools available. And by extension, maybe in our more complete type system there are things which can't be proven yet, but could perhaps be if there were better tools available? Maybe another angle to look at it: one of the things which is difficult to prove is the halting problem. Maybe you can't prove that a given program will terminate. But you could run that program and watch it terminate, and then you'd know it does. In that sense there is a "true" answer, but one which couldn't have been proved in advance from type theory. But I admit I only have a high-level understanding of these things. Type theory and axiomatic mathematics is something I'd like to know more about.

UncleMeat 5y ago

> If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. This depends on your formalism for logic. Intuitionist logic merges the meaning of "true" and "has a proof" but classical logic does not have any problem with having a thing be called "true" while also not being provable.

rocqua 5y ago

I believe most constructive mathematics (mathematics not using the law of the exluded middle) is actually weaker than peano arithmetic. Certainly there is less that has been proven in it. Most type theory is constructive afaik, hence it might be weaker than even Godel implies.

zozbot234 5y ago
Constructive mathematics can prove anything that classical mathematics can, and more. The only catch is that propositions which are proven classically must always be stated in the negative fragment of the logic: there's no general duality as there is in classical logic, but a positive and a negative statement mean something different.
- Koshkin 5y ago
  > and more I am not sure about that - there are some "pathological" phenomena in classical math that are rejected (for the lack of proof) in constructive math.
  - deleted 5y ago
    [deleted]
- rocqua 5y ago
  How does this work for the banach tarski paradox?
  - zozbot234 5y ago
    That depends on the axiom of choice. From a constructive POV, this means you would have to introduce some sort of extra assumptions to the theorem itself. (The axiom of choice is also inconsistent with some popular extensions to constructive mathematics, so Banach-Tarski simply cannot apply to those mathematical objects.)

auggierose 5y ago

ZFC comes with First-Order Logic and is certainly complete. You are right in that sense. Let me be more specific: Given a sentence that is true in every model of ZFC, you can prove that sentence. This is true because ZFC is a first-order theory, and this is a property of ANY first-order theory. People that are pointing out incompleteness are talking about something else: They are talking about the fact that there are sentences S where neither S nor not S is provable. Additionally, there is a meta reason why S is believed to be true. For example, take S = encoding of "ZFC is consistent". BUT: This sentence S is true in some models of ZFC, and false in others, because otherwise the completeness of ZFC would make it provable / disprovable. So this boils down to the meta-truth being different from truth in a model. Disclaimer: I just recently looked seriously into this stuff, because I was wondering about completeness of a logic I invented. So if the above is wrong, please somebody correct me!

rssoconnor 5y ago

There are true (in the sense of Tarski's definition of truth) but unprovable (Π₁) sentences in any consistent (sufficiently powerful) system. Which of these true sentences are unprovable varies from system to system. Π₁-sentences (see arithmetical hierarchy) are closed formulas of the form, ∀x:ℕ. P(x), where P is some decidable predicate. i.e. all quantifiers in P are bounded. Thus for any given fixed value for x, say n, P(n) can be expanded out into conjunctions and disjunctions of atomic equalities and inequalities between closed arithmetic formula and those (in)equalities can in turn be decided (in principle) by calculation. Notice that 'x' is a formal variable in the language of first order logic, while we are using 'n' as a meta-variable denoting a term representing a numeral, e.g. 42. Σ₁-sentences are closed formulas of the form, ∃x:ℕ. P(x), where P is again a decidable predicate. Some basic first order logic yields that the negation of a Σ₁-sentence is logically equivalent to a Π₁-sentences and similarly the negation of a Π₁-sentence is logically equivalent to a Σ₁-sentence. Important Fact: All true Σ₁-sentences are provable (in any sufficiently powerful system). Why? Suppose ∃x. P(x) is true. Then, there is some numeral 'n' where P(n) is true. Since P(n) is decidable we can prove P(n) when P(n) is true. And, by the rule of existential introduction, ∃x.P(x) is provable from P(n). Now, let us consider some consistent system T (which is "sufficiently powerful"). For example, we can take T to be ZFC if you think ZFC is consistent. We can construct a Goedel-Rosser sentence for T, let's call this sentence G. G is a Π₁-sentence by construction, so we can put G in the form of ∀x:ℕ. P(x) for some decidable predicate P. Now either G is true, (i.e. ∀x:ℕ. P(x) is true) or ¬G is true, (i.e. ∃x:ℕ. ¬P(x) is true). Suppose ¬G is true. Since ¬G is (equivalent to) a Σ₁-sentence then T proves ¬G. But by the Goedel-Rosser incompleteness theorem, this would imply that T is inconsistent, contradicting our assumption. Thus it must be the case that G is true. However G is unprovable in T because, again by the Goedel-Rosser incompleteness theorem, if G were provable in T, then T would be inconsistent, contradicting our assumption. Thus G is an example of a true sentence that isn't provable in T.

ProfHewitt 5y ago
The halting problem provides examples of true but unprovable propositions because there are some expressions that do not halt but it is unprovable that they do not halt.
5y ago