[TYPES] Encoding of negation

[Philip Wadler]

One possible encoding of negation, closely related to the CPS  
translation, is the following:

   A*         =  all Z. A+

   X+         =  X
   (A -> B)+  =  A+ -> B+
   (not A)+   =  A+ -> Z

where Z is a fresh type variable that does not appear free in A.  I  
conjecture that

   A1, ..., An |- B

holds in classical logic iff

   A1*, ..., An* |- B*

holds in intuitionistic logic.

Has anyone explored this translation?  As an example of its interest,  
I conjecture that A* and (not (not A))* are isomorphic in the  
presence of parametricity; this is certainly true if A contains no  
negations.

Many thanks for any responses.  Cheers,  -- P