On 17-05-20 21:00, Kim-Ee Yeoh wrote:
But what about the Curry-Howard correspondence for classical logic?
Curry-Howard only offers a translation between a fragment of logic that is constructive logic and the typed lambda calculus. But that is not the whole story, we can embed classical logic into constructive logic via the the "double negation translation" [1]. How is such thing possible? The idea is that classical logic is constructive logic with an extra axiom. That extra axiom can either be Pierce's Law, the excluded middle or the double negation elimination. Which ever you "add" to your constructive logic will make it a classical logic. Here is the trick, to whatever proposition `a` that we want to prove, we can "add" an extra postulate for a non-local jump as an argument and call that proposition `CPS a`. That way, when proving/constructing the term inside the CPS-code, you will have at your hand an extra argument that will allow you to fill the extra power needed by classical proofs [1]. It's interesting to note that operationally, what classical proofs can do that constructive proofs cannot is the ability to do non-local jumps, there represented by the continuation. Harper's course given at [2] has been my fun the last few days and explains it in greater detail.
What would the classical code for the classical proof of excluded middle look like?
As in the previous mails type Not a = a -> Void type CPS a = (a -> Void) -> Void proof :: CPS (Either a (Not a)) proof = \cont -> cont $ Right (\a -> cont (Left a)) Modulo my point between the different representations of CPS and their relation to the double negation, that code only type check because terms under CPS have access to an extra non-local jump to allow classical arguments. Even so this code is *good* as shows explicitly when the non-local jumps happen and the rest of the code is constructive. [1]: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/class.pdf [2]: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts -- -- Rubén -- pgp: 4EE9 28F7 932E F4AD