[Agda] Parametricity is inconsistent with classical logic

[Benja Fallenstein]

Hi all,

On Fri, Apr 20, 2012 at 12:46 PM, Arseniy Alekseyev
<arseniy.alekseyev at gmail.com> wrote:
> I've noticed that parametricity postulates are inconsistent with
> classical logic, that is if you postulate both parametricity and the
> law of excluded middle, you can derive a contradiction.

Interesting, I for one hadn't realized that!

If you don't need choice, it seems that you should be able to
circumvent this by using the style proposed by Russell O'Connor in
"Classical Mathematics for a Constructive World":

http://arxiv.org/pdf/1008.1213v2

Since in that approach you don't add any axioms for basic classical
reasoning, there shouldn't be a problem with parametricity.

On the other hand, if you add the classical axiom of choice -- my own
prefered version of writing it would be

> postulate choice : {k l : Level} → {X : Set k} → {F : X → Set l} → ((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)

-- then it seems you'd run into problems again: given

> data Either (X Y : Set) : Set where
>   left : X → Either X Y
>   right : Y → Either X Y
>
> _∨_ : Set → Set → Set
> X ∨ Y = ¬ ¬ Either X Y

you can prove

> tnd : (X : Set) → X ∨ ¬ X

and using choice, you get

> bad : ¬ ¬ ((X : Set) → X ∨ ¬ X)

It's not entirely obvious to me whether you can derive a contradiction
to parametricity from this, but in the intended kind of classical
model, this type is inhabited iff ((X : Set) → X ∨ ¬ X) is, so even if
this were consistent with parametricity it wouldn't have the right
semantics...

Good to know.

Cheers,
- Benja