[Agda] Re: Classical Mathematics for a Constructive World

[Liang-Ting Chen]

On 20 November 2012 13:28, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

> On 20/11/12 12:03, Jan Burse wrote:
>
>> Diaconescu's Theorem
>> http://en.wikipedia.org/wiki/**Diaconescu%27s_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/<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.
>
After Martin's reply, I just want to mention the following article by Per
Martin-Löf which explains that the "extensional" choice / Zermelo's choice
imply excluded middle in MLTT:

Martin-Lof, 100 years of Zermelo's axiom of choice: what was the problem
with it?, 2006 http://comjnl.oxfordjournals.org/content/49/3/345.extract


> 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
>
>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>



-- 
Liang-Ting Chen, PhD student
School of Computer Science,
The University of Birmingham, UK
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121120/374878a6/attachment.html