[TYPES] Encoding of negation

[Vladimir Komendantsky]

On Sat, Aug 25, 2007 at 10:59:54AM +0100, Philip Wadler wrote:
> So you are suggesting that my conjecture may hold if we modify it as  
> follows:
> 
> A* = all Z. A+ -> Z
> 
> A+ as before

No, even then your conjecture wouldn't hold, as you do note below:

> This in effect adds a negation, so I would no longer expect
> that A1,...,An |- B classically iff A1*,...,An* |-  B*  
> intuitionistically,
> although I might expect that A |- B classically iff B* |- A*  
> intuitionistically.

You couldn't have ever expected Gamma |- B classically iff Gamma* |- B*
intuitionistically because this is false for your definition of *.

Your point about A |- B iff B* |- A* is fair. This can certainly be exploited
for a number of purposes.

> Why do you claim that if the above is provable then (A\/B)->A is  
> provable?  Note that in the case where A does not contain negation,  
> all Z. (A+ -> Z) -> Z is isomorphic to A, in the presence of  
> parametricity.

I do so because of the following intuitionistic reasoning:

1.  all Z. (A+ -> Z) -> Z) |- all Z. A+
2.  (A+ -> B) -> B |- A+               (eliminate "all")
3.  (C \/ D) |- (C -> D) -> D          (intuitionistic fact)
4.  (A+ \/ B) |- A+                    (apply transitivity of |- to 3 an 2)

3 and 4 are not related to the direct counterexample, which was noted by Rowan
earlier in this discussion. However, 4 shows your translation not being
faithful.

The direct counterexample is simply 1 and 2. The statement at 1 is neither
intuitionistically nor classically provable. 2 is a simplier presentation
for 1.

--
Vladimir