[Agda] Re: Classical Mathematics for a Constructive World

[Martin Escardo]

On 20/11/12 12:03, Jan Burse wrote:
> 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?

That "choice implies excluded middle" causes much confusion indeed.

See e.g. http://plato.stanford.edu/entries/mathematics-constructive/

In MLTT type theory, and in Agda, you can prove choice but you can't 
prove excluded middle. In particular, choice doesn't imply excluded middle.

In intuitionistic set theory, choice implies excluded middle. But 
restricted forms of choice (e.g. countable choice, dependent choice) don't.

In general, the situation is "assuming X, choice implies excluded 
middle", where people don't mention X.

This probably isn't the right place for a full discussion.

But, in summary, a derivation of excluded middle is ruled out in the 
Agda material you are referring to.

Best,
Martin