Hacker News new | past | comments | ask | show | jobs | submit login

You won't convince anyone of this until they start working heavily in a theorem prover. With constructive proofs you can introduce certain automation that is not possible otherwise; until then, when we are working on pen and paper, it is a limitation on your proof techniques.

But you are are aware of this already, I'm just writing it out.






I'm surprised by this statement. Most of the research in automatic theorem proving (including for first and higher order logics) is based on classical logic, because it's much easier to reduce to a search for false, than to try and prove an arbitrary formula. The automatic provers able to do intuitionistic proofs generally do it by encoding the intuitionistic logic into a classical logic first.

Look at these provers, they're almost all based on classical logic, and even on proofs by contradiction: http://www.tptp.org/CASC/27/SystemDescriptions.html

Even Isabelle/HOL, which is quite user friendly and has a lot of automation (like Sledgehammer, which can call to the automatic provers mentioned above) is based on classical logic with choice.


Hmm, I was more thinking about proof translation across isomorphisms. I'm not speaking from my own experience here, just that I have seen people grumble about it.

https://leanprover-community.github.io/archive/113488general...


:-). I agree. Sure constructive proofs are sometimes longer, but it's the computer doing most of the work.

But you also end up with proofs that are much, much shorter.

I guess it's all about the degree of uncertainty. Constructive mathematics reduces the degree of uncertainty, which grows exponentially as you get in the higher level proofs.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: