[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

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
http://en.wikipedia.org/wiki/Diaconescu%27s_theorem

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

Bye