[Agda] Agda with the excluded middle is inconsistent ?

[Thierry Coquand]

 The impredicative version(s) of the proof have some similarity with a discussion of
(Bertrand) Russell in Appendix B of Principles of Mathematics (1903?). With type theoretic
notations, Russell argues first that the function

 forall : (Prop -> Prop) -> Prop

should be one-to-one ("Let n be different from m, 'every n is true' is not the same
proposition as 'every m is true'."). He then forms the class of proposition P : Prop -> Prop

 P u = exists m: Prop -> Prop.   u = forall m   &    not (m u)

and deduces a contradiction.

 He then discusses this contradiction (starting "In order to deal with this contradiction, it is desirable
to reopen the question of the identity of equivalent propositional functions and of the nature
of the logical product of two propositions") but without any definite conclusion.

               Best regards,

                  Thierry




> Hi Russel,
> 
> I posted a similar proof yesterday, which is originally from Alexandre Miquel's idea.