[Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Wed Nov 21 11:07:30 CET 2012

Jan Burse schrieb:
> 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?

In your logical framework and for your choice principle,
how often does it happen that it can be replaced
by an induction. Is it possible to identify some broad
class of problems where this is possible?


More information about the Agda mailing list