5 ms·

This is fascinating, but only if you hold faith in inherent truth of mathematical symbolism. Unfortunately, this seems to be the standard dogma of mathematician

This is fascinating, but only if you hold faith in inherent truth of mathematical symbolism. Unfortunately, this seems to be the standard dogma of mathematicians, though I haven't seen significant evidence necessary to warrant this belief. If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

popnroll 8y ago
I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?
- protonfish 8y ago
  No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
  - mietek 8y ago
    > It shows that no significantly expressive system can be designed that won't allow paradoxical statements. The above is a complete misrepresentation of Gödel’s second incompleteness theorem. The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means. Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8]. All of these languages are designed to be consistent. Of course, implementation bugs do happen[9]. If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11]. [1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_conditions https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co... [2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems#Second_incompleteness_theorem https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor... [3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [5] Agda programming language, http://agda.readthedocs.io http://agda.readthedocs.io [6] Coq proof assistant, http://coq.inria.fr http://coq.inria.fr [7] Idris programming language, http://www.idris-lang.org http://www.idris-lang.org [8] Lean theorem prover, http://leanprover.github.io http://leanprover.github.io [9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408 https://twitter.com/i/moments/921153475836305408 [10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer [11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming
    - commanderjroc 8y ago
      I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent. To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T. So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system. In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.
  - TheRealPomax 8y ago
    Unprovable statements. Not paradoxical statements. Paradoxes confound the reader, but can be explained as either being true or false due to rules that were implicitly used to construct the statement. Once all the steps are explicitly shown, with each rule that applies at each step, there is no more paradox. On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent. The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system". While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.
- cyphar 8y ago
  No, this is more about the philosophy of mathematics -- the question of "to which degree is mathematics 'real'?" Gödel did have an impact on this, with formalism no longer being a particularly viable viewpoint. But this is less of a strict mathematical question and more of a philosophical one.
- undershirt 8y ago
  The struggle is that the symbolic graphs we construct to explain facts become logical beasts of their own, prone to generating sentences paradoxical under our desired interpretation. Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another. But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning. Gödel seems very much related to this, but I'm still lost.
jrochkind1 8y ago
Of course, the reason we invest so much in mathematics is because it is somewhat mysteriously effective for describing the observed world, not just because it's an arbitrary formalized language of symbols. "The Unreasonable Effectiveness of Mathematics in the Natural Sciences" by Eugene Wigner https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.html https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.htm... > The first point is that mathematical concepts turn up in entirely unexpected connections. Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections. Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate. We are in a position similar to that of a man who was provided with a bunch of keys and who, having to open several doors in succession, always hit on the right key on the first or second trial. He became skeptical concerning the uniqueness of the coordination between keys and doors. > Most of what will be said on these questions will not be new; it has probably occurred to most scientists in one form or another. My principal aim is to illuminate it from several sides. The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it. Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories. (The article happens to mention the Brouwer-Hilbert controversy but only in a footnote).
- protonfish 8y ago
  That essay is a significant source of belief in the myth of inherent mathematical truth, but it has flaws and is far from proof. It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable. Most importantly, the leap that if a medium can be used to create accurate representations, it must contain inherent, unquestioning truth about that represented phenomena, is just hogwash. Michelangelo could sculpt masterful representations of the human form, but the beauty and accuracy of the representation are the products of a skilled master, not the inherent humanness of marble.
  - 8y ago
dwohnitmok 8y ago
I dunno if I'd call it dogma. For the most part, most working mathematicians I've run into basically don't care either way and adaptively adopt whichever philosophy happens to match best with their intuition for a particular problem. This can change on a problem by problem basis. I wouldn't be surprised if a working mathematician hadn't heard of intuitionism or formalism. Interestingly, your latter point is exactly formalism (the "formal" part is referring to the formalized language), i.e. Hilbert's position. Formalism basically asserts that mathematics is a fancy string manipulation game.
canhascodez 8y ago
There is no one thing called "truth". There are different systems of verification, which produce truths, but "1 + 1" is not comparable to "water boils at 100 degrees C". Mathematics fundamentally does not describe the real world. It models the real world--and many other worlds besides. Mathematical truths describe axiomatic systems. The properties of the real world are determined not by mathematics, but by measurement. > The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing. This is usually called "physics".

popnroll 8y ago

I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?

protonfish 8y ago
No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
- mietek 8y ago
  > It shows that no significantly expressive system can be designed that won't allow paradoxical statements. The above is a complete misrepresentation of Gödel’s second incompleteness theorem. The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means. Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8]. All of these languages are designed to be consistent. Of course, implementation bugs do happen[9]. If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11]. [1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_conditions https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co... [2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems#Second_incompleteness_theorem https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor... [3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [5] Agda programming language, http://agda.readthedocs.io http://agda.readthedocs.io [6] Coq proof assistant, http://coq.inria.fr http://coq.inria.fr [7] Idris programming language, http://www.idris-lang.org http://www.idris-lang.org [8] Lean theorem prover, http://leanprover.github.io http://leanprover.github.io [9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408 https://twitter.com/i/moments/921153475836305408 [10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer [11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming
  - commanderjroc 8y ago
    I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent. To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T. So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system. In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.
- TheRealPomax 8y ago
  Unprovable statements. Not paradoxical statements. Paradoxes confound the reader, but can be explained as either being true or false due to rules that were implicitly used to construct the statement. Once all the steps are explicitly shown, with each rule that applies at each step, there is no more paradox. On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent. The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system". While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.
cyphar 8y ago
No, this is more about the philosophy of mathematics -- the question of "to which degree is mathematics 'real'?" Gödel did have an impact on this, with formalism no longer being a particularly viable viewpoint. But this is less of a strict mathematical question and more of a philosophical one.
undershirt 8y ago
The struggle is that the symbolic graphs we construct to explain facts become logical beasts of their own, prone to generating sentences paradoxical under our desired interpretation. Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another. But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning. Gödel seems very much related to this, but I'm still lost.

jrochkind1 8y ago

Of course, the reason we invest so much in mathematics is because it is somewhat mysteriously effective for describing the observed world, not just because it's an arbitrary formalized language of symbols. "The Unreasonable Effectiveness of Mathematics in the Natural Sciences" by Eugene Wigner https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.html https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.htm... > The first point is that mathematical concepts turn up in entirely unexpected connections. Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections. Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate. We are in a position similar to that of a man who was provided with a bunch of keys and who, having to open several doors in succession, always hit on the right key on the first or second trial. He became skeptical concerning the uniqueness of the coordination between keys and doors. > Most of what will be said on these questions will not be new; it has probably occurred to most scientists in one form or another. My principal aim is to illuminate it from several sides. The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it. Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories. (The article happens to mention the Brouwer-Hilbert controversy but only in a footnote).

protonfish 8y ago
That essay is a significant source of belief in the myth of inherent mathematical truth, but it has flaws and is far from proof. It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable. Most importantly, the leap that if a medium can be used to create accurate representations, it must contain inherent, unquestioning truth about that represented phenomena, is just hogwash. Michelangelo could sculpt masterful representations of the human form, but the beauty and accuracy of the representation are the products of a skilled master, not the inherent humanness of marble.
- 8y ago

dwohnitmok 8y ago

I dunno if I'd call it dogma. For the most part, most working mathematicians I've run into basically don't care either way and adaptively adopt whichever philosophy happens to match best with their intuition for a particular problem. This can change on a problem by problem basis. I wouldn't be surprised if a working mathematician hadn't heard of intuitionism or formalism. Interestingly, your latter point is exactly formalism (the "formal" part is referring to the formalized language), i.e. Hilbert's position. Formalism basically asserts that mathematics is a fancy string manipulation game.

canhascodez 8y ago

There is no one thing called "truth". There are different systems of verification, which produce truths, but "1 + 1" is not comparable to "water boils at 100 degrees C". Mathematics fundamentally does not describe the real world. It models the real world--and many other worlds besides. Mathematical truths describe axiomatic systems. The properties of the real world are determined not by mathematics, but by measurement. > The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing. This is usually called "physics".