<br><br><div class="gmail_quote">On 20 November 2012 13:28, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 20/11/12 12:03, Jan Burse wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Diaconescu's Theorem<br>
<a href="http://en.wikipedia.org/wiki/Diaconescu%27s_theorem" target="_blank">http://en.wikipedia.org/wiki/<u></u>Diaconescu%27s_theorem</a><br>
<br>
Do you think the choice principle and the rest of the<br>
logical framework you used, excludes a derivation of<br>
the excluded middle?<br>
</blockquote>
<br></div>
That "choice implies excluded middle" causes much confusion indeed.<br>
<br>
See e.g. <a href="http://plato.stanford.edu/entries/mathematics-constructive/" target="_blank">http://plato.stanford.edu/<u></u>entries/mathematics-<u></u>constructive/</a><br>
<br>
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.<br>
<br>
In intuitionistic set theory, choice implies excluded middle. But restricted forms of choice (e.g. countable choice, dependent choice) don't.<br></blockquote><div>After Martin's reply, I just want to mention the following article by <span style="font-family:inherit;font-size:inherit;font-style:inherit;line-height:inherit;background-color:rgb(255,255,255);color:rgb(34,34,34)">Per Martin-Löf</span> which explains that the "extensional" choice / Zermelo's choice imply excluded middle in MLTT:</div>
<div><br></div><div>Martin-Lof, 100 years of Zermelo's axiom of choice: what was the problem with it?, 2006 <a href="http://comjnl.oxfordjournals.org/content/49/3/345.extract">http://comjnl.oxfordjournals.org/content/49/3/345.extract</a></div>
<div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
In general, the situation is "assuming X, choice implies excluded middle", where people don't mention X.<br>
<br>
This probably isn't the right place for a full discussion.<br>
<br>
But, in summary, a derivation of excluded middle is ruled out in the Agda material you are referring to.<br>
<br>
Best,<br>
Martin<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><font style="color:rgb(0,0,0)" color="#888888"><span>Liang-Ting Chen</span>, PhD student<br><div>School of Computer Science,<br>The University of Birmingham, UK</div>
</font><br>