[Agda] Parametricity is inconsistent with classical logic

[Danko Ilik]

On Wed, May 09, 2012 at 11:27:58AM +0200, Nils Anders Danielsson wrote:
> >>>postulate choice : {k l : Level} → {X : Set k} → {F : X → Set l} →
> >>>((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)
> >
> >This corresponds to Spector's Double Negation Shift principle.
> 
> Not for arbitrary types X, right? See the following message:
> 
>   Martin Escardo
>   Re: Agda with excluded middle is inconsistent
>   http://thread.gmane.org/gmane.comp.lang.agda/1367/focus=1407

Well, in pure intuitionistic predicate logic. If you add (arithmetic) axioms and you allow X to be ℕ→ℕ, then you may get inconsistency with some continuity principles. But, even if you only let X=ℕ you get into trouble (depending on what you consider trouble:), because you can show certain formal versions of Church's Thesis to be false.

Martin Escardo's argument is that you will not be able to use bar recursion to justify DNS for X≠ℕ, but it does not mean that you could never possible justify it. It seems that with control operators in logic you can do something (ex. http://hal.inria.fr/hal-00647389) 

Cheers,
Danko