This seems important and interesting but I think I need an essay length explanation. Is there one?
-
-
Back to the point though: The axiom of the excluded middle isn't provable in constructive logic, and you can not use constructive logics to prove theorems with it without explicitly assuming it. You can use constructive logic to prove that other logics prove theorems using it.
-
What this means is that simulating non-constructive logic inside a constructive logic doesn't give you a way to build a constructive proof from your non-constructive proofs. CC simulates the proof checker, not the proof
- 15 more replies
New conversation -
-
-
I sometimes like to use the idea of a derivative here. A line cannot be reified, but it’s derivative can. Pi cannot be reified, but a algorithm to compute it can. An infinite set cannot be reified, but can be specified. Etc. The difference between classic and constructive math?
-
It would seem that continuous integration is a bit fishy, yes… I think about it as difference between specification and implementation.
End of conversation
New conversation -
-
-
Similarly, ultrafinitism says whereof we cannot speak a number, thereof we must be silent, but every number we every encounter will be ultrafinitistically viable.
-
In practice, making that demand does not seem viable, we need probabilistically relaxed mathematics, i.e. in areas where we cannot be certain to be able to construct a proof, we can introduce axioms that are defined as "true until proven otherwise".
End of conversation
New conversation -
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.