[TYPES] Encoding of negation
Vladimir Komendantsky
v.komendantsky at bcri.ucc.ie
Sat Aug 25 12:37:34 EDT 2007
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
More information about the Types-list
mailing list