[Agda] Parametricity is inconsistent with classical logic

Arseniy Alekseyev arseniy.alekseyev at gmail.com
Fri Apr 20 12:46:08 CEST 2012


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. Although it is
obvious in retrospect (lem, polymorphic in A, can not possibly know
whether to produce "yes" or "no" while being parametric!), I've never
heard it before, so i'm asking:

Is this a known fact?

Arseniy.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: parametricity.agda
Type: application/octet-stream
Size: 2343 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120420/771f6024/parametricity.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: parametricity2.agda
Type: application/octet-stream
Size: 2601 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120420/771f6024/parametricity2.obj


More information about the Agda mailing list