[TYPES] Re: Encoding of negation

[Vladimir Komendantsky]

>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.
>

A closely related call-by-name CPS translation was described, e.g., in 
Peter Selinger's "Control categories and duality: on the categorical 
semantics of the lambda-mu calculus" (2001), 
http://www.mscs.dal.ca/~selinger/papers/control.pdf

There, in Section 6.1, he gives the CPS translation which, if we content
ourselves with the case above, gives the following rules for translation
of types:

A* = A+ -> R
X+ = X
(A->B)+ = A+ -> B+
(not A)+ = A+ -> R

where R is a free fixed type variable (the type of responses). The
difference is in A* which now has an occurrence of R in it.

So, for example, the law of double negation elimination

(not (not A)) |- A

is translated as

((A+ -> R) -> R) -> R |- A+ -> R.

Since this translation is call-by-name, it is not directly related to
Hayo Thieleke's CPS translation, which is call-by-value. The idea behind
the call-by-name CPS translation stems back to Goedel's double negation
translation. The variants of the CPS call-by-value translation 
correspond (sometimes loosely) to Kolmogorov's double negation
translation. As noted by Hayo Thieleke, in the absence of control types
(which is exactly the case) one has universal quantification, "all Z",
instread of just the free variable R.

>I conjecture that
>
>   A1, ..., An |- B
>
>holds in classical logic iff
>
>   A1*, ..., An* |- B*
>
>holds in intuitionistic logic.
>
>  
>
For Peter Selinger's translation above this holds if we rewrite R with
_|_. But if we let

A* = all Z. A+

(and don't rewrite response variables) we obtain the following
translation of the double negation elimination:

all Z. (A+ -> Z) -> Z) |- all Z. A+

This is not provable already in classical logic (otherwise (A\/B)->A
would be provable). In this sence the above conjecture does not hold.


--
Vladimir