[Agda] Parametricity is inconsistent with classical logic

[Martin Escardo]

On 10/05/12 19:11, Danko Ilik wrote:
> Do you have some references about results about ¬LPO?

Let's take this off line.

> Regarding ¬¬LPO, maybe one obtains something more if one defines "¬"
> as "→S" where S is a Σ⁰₁-formula, instead of plainly as "→⊥" using the
> not very informative absurdity atom. Actually, one may prove DNS for
> the first kind of negation, and consequently also ¬¬LPO.

But I can't resist making a comment about this point. Actually, before 
writing the previous reply, I tried to do precisely what you say in the 
above paragraph. But I don't think it works, because to prove ¬¬LPO one 
uses ⊥→P for suitable P at some point, and if I am not mistaken, this is 
unavoidable. (If you could do that for arbitrary S, you could then do it 
for S=LPO, and then LPO follows. But LPO is not a Σ⁰₁-formula.)

Martin