> 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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.