[Agda] Parametricity is inconsistent with classical logic
Martin Escardo
m.escardo at cs.bham.ac.uk
Fri May 11 10:11:34 CEST 2012
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
More information about the Agda
mailing list