Gödel and Turing: we cannot use classical mathematics to build an interpreter that runs classical mathematics Church and Turing: we can use constructive mathematics to run constructive mathematics Minsky and Turing: we can use constructive mathematics to run classical mathematics
-
-
since we cannot know that our interface to the machine is entirely coherent, we may always have to bracket our theories into a residual probability that a bit flipped somewhere in the proof making machine or its verification machine or the interpretation of the verification, etc
-
the main claim of AI and cognitive science however is that the brain is a computer, and because all the mathematics we need to account for run on our brains, we can build something that can satisfy all desires a classical mathematician can hope to fulfill with a finite automaton
- 20 more replies
New conversation -
-
-
Intuitionistic logic does not mean you need to actually run the proof, just that a theoretical machine could run it. You can in fact have proofs about all numbers, that 2 * n is even. The proof here is a function & you don't need to try it on all numbers to know it is correct
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Ah got it.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.