[Agda] Parametricity is inconsistent with classical logic

[Danko Ilik]

On Thu, May 10, 2012 at 10:21:44AM +0100, Martin Escardo wrote:
> Interesting indeed. Although I don't understand the technical
> details (I lack enough background on delimited continuations), the
> claims you make in the paper do seem plausible, and I trust you.

Thank you for your comments! There is an alernative proof of
normalization and disjunction and existence properties that is more
semantical (and formalised in Coq), so I am pretty sure of the result.

> What puzzles me is that one can prove, from the DNS for the type
> X=(N->2), the principle ¬¬LPO, where LPO is the claim that every
> infinite binary sequence is either constantly zero or has a
> one. LPO solves the Halting Problem, and ¬LPO is consistent with
> type theory. So ¬¬LPO says that it is ridiculous to assume one
> cannot solve the Halting Problem, but stops short of providing a
> solution.

Yes, with Keiko Nakata we also noticed that ¬¬LPO becomes
derivable. Actually, more generally, as I learned from Veldman, DNS is
equivalent to ¬¬∀n(A(n)∨¬A(n)) for any A(n).

> It seems strange that you can make a constructive system branch
> into two constructive systems, one with the extension ¬LPO and the
> other with its negation ¬¬LPO, but I suppose I have to accept
> that. It is well known that ¬LPO is equivalent to a continuity
> axiom: all functions are continuous in a certain sense. Hence
> ¬¬LPO says that not all functions are continuous (but doesn't give
> a counter example, whereas LPO does, although LPO is a taboo).

Do you have some references about results about ¬LPO?

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.

Danko