Hacker News new | ask | show | jobs
by librexpr 1238 days ago
You might want to check out the Gödel–Gentzen negative translation[0], which is an interpretation of classical logic in intuitionistic logic, which can be (somewhat inaccurately) summarized as "if P is provable in classical logic, then not not P is provable in intuitionistic logic".

[0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...