[TYPES] Encoding of negation
Philip Wadler
wadler at inf.ed.ac.uk
Fri Aug 24 14:34:13 EDT 2007
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
More information about the Types-list
mailing list