[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

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?

Bye