2. Double negation enables a translation of classical logic in intuitionistic logic, here embedded in Haskell:
Below I'll give a variant of Li-yao's logic language in Haskell98. Again, the open set model may help to visualize CPS translation: Consider all open sets A on the real line which are fixed points of double negation. All intervals are of this kind, but poking holes in them destroys this property: ---(====)(====)--- A ===)----------(=== Not A ---(==========)--- Not (Not A) Denote the collection of open sets invariant under double negation by X. As the example above demonstrates, X is not closed under set union. But set intersection preserves membership of X. So we have a funny logic that has (&&) but no (||). The CPS trick is now to define a new (||) by means of double negation: ---(====)--------- A ---------(====)--- B ---(====)(====)--- set union of A and B ---(==========)--- A || B, double negation of set union. In fact X is the largest Boolean algebra contained in the Heyting algebra of open sets. In terms of Haskell, we define a new Either: Either' a b = ((Either a b) -> Void) -> Void Looks familiar? Indeed, in this thread we already proved Either' a (Not a). This says that Not A is the Boolean complement of A in X. Using (,) and Either' for (&&) and (||) you can realize all proofs of classical propositional logic in Haskell without GADTs. Olaf