[TYPES] Encoding of negation

[Philip Wadler]

Many thanks to Alex Simpson, Noam Zeilberger, and Hasegawa Masahito  
for pointing out that my conjecture cannot be correct (see below),  
and to Carter Schonwald, Burak Emir, Thomas Streicher, and Vladimir  
Komendanstsky for pointing to results related to the conjecture.  Any  
other pointers appreciated.  Cheers, -- P

On 21 Aug 2007, at 16:59, Noam Zeilberger wrote:

>> 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.
>
> I don't think the above is the right translation of implication,
> because this conjecture is easily falsified by negation-free
> classical theorems which are not intuitionistic.  For example,
> Pierce's law P = ((X -> Y) -> X) -> X is valid classically,
> but P* = all Z.P is not valid intuitionistically.
>
> I guess a natural fix would be to use
>
>    (A -> B)+ = A+ -> (B+ -> Z) -> Z
>
> Then the translation of Pierce's law becomes:
>
>  P* = all Z.((X -> (Y -> Z) -> Z) -> (X -> Z) -> Z) -> (X -> Z) -> Z
>
> Kind of an eyesore, but indeed intuitionistically valid.
>
> Noam