[Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Tue Nov 20 13:03:20 CET 2012

Jan Burse schrieb:
> Martin Escardo schrieb:
>> The following Agda code is related:
>> http://www.cs.bham.ac.uk/~mhe/pigeon/
>> It uses the generalized double negation monad X |-> (X->R)->R to code a
>> classical proof in Agda (without postulating excluded middle).
>> Martin
> Do you think, since it is not postulated, it is not
> derivable via some of the translations given in the paper?
> Bye

Diaconescu's Theorem

Do you think the choice principle and the rest of the
logical framework you used, excludes a derivation of
the excluded middle?


More information about the Agda mailing list