4 ms·

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpres

by szany 11y ago

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

joe_the_user 11y ago
"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof system admits an uncountable sets of independent theorems and so-forth.
- szany 11y ago
  Most true statements are uninteresting.
  - joe_the_user 11y ago
    Indeed but so are most programs.
- mafribe 11y ago
  While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.
  - joe_the_user 11y ago
    It doesn't follow in normal mathematical practice I think because mathematicians want natural, sane axioms that lead to human understandable models. Computing already starts out much messier in its activities. Determining what will happen when a large system gets input is tricky. I'm not sure what could proved about the operations of a "deep neural net" for example.
- kazinator 11y ago
  Unfortunately, that isn't a world in which you could connect a USB camera to your laptop and just have it work after the system finds the right driver.
- jonsterling 11y ago
  Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.
  - joe_the_user 11y ago
    I'm pretty sure if you are talking about proofs having to do with a determined, computation system, Godel applies. I mean, the unsolvability of the halting problem certainly applies and this gives a somewhat similar picture of the world.
    - jonsterling 11y ago
      In bob's setting, the computation system is not determined or fixed. It is open-ended... In intuitionistic mathematics, we of course accept that there is no Turing computable halting oracle, but we do not rule out the possibility that there is some other effective oracle that can decide halting. (This is in contrast to recursive mathematics / Russian constructivism)

by szany 11y ago

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

joe_the_user 11y ago

"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof system admits an uncountable sets of independent theorems and so-forth.

szany 11y ago
Most true statements are uninteresting.
- joe_the_user 11y ago
  Indeed but so are most programs.
mafribe 11y ago
While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.
- joe_the_user 11y ago
  It doesn't follow in normal mathematical practice I think because mathematicians want natural, sane axioms that lead to human understandable models. Computing already starts out much messier in its activities. Determining what will happen when a large system gets input is tricky. I'm not sure what could proved about the operations of a "deep neural net" for example.
kazinator 11y ago
Unfortunately, that isn't a world in which you could connect a USB camera to your laptop and just have it work after the system finds the right driver.
jonsterling 11y ago
Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.
- joe_the_user 11y ago
  I'm pretty sure if you are talking about proofs having to do with a determined, computation system, Godel applies. I mean, the unsolvability of the halting problem certainly applies and this gives a somewhat similar picture of the world.
  - jonsterling 11y ago
    In bob's setting, the computation system is not determined or fixed. It is open-ended... In intuitionistic mathematics, we of course accept that there is no Turing computable halting oracle, but we do not rule out the possibility that there is some other effective oracle that can decide halting. (This is in contrast to recursive mathematics / Russian constructivism)