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

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...




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

Search: