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
-
-
construction means that there has to be a machine that can perform the actual computations. in the strong, intuitionist form, we must actually run the proof, i.e. we need to compress it into a form that actually runs on our machine (which leads to a small foundational crack)
-
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
- 21 more replies
New conversation -
-
-
The axiom of choice holds in (probably the most common) constructive logic: https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Also, constructive math does not prevent functions from being numbers. You can still add codata and calculate with 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.