<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif; "><div>Hi,</div><div><br></div><div>I have never been happy with Per's view that Diaconescu's construction has anything to do with extensionality. My explanation is that it is the propositional axiom of choice which is the problem. Let me explain: As Martin already remarked in Type Theory the axiom of choice is provable in the following form (GIven A,B : Set and R : A -> B -> Prop), where by Prop I mean sets with at most one inhabitant (HProp?):</div><div><br></div><div>ac :<span class="Apple-tab-span" style="white-space:pre"> </span>((a : A) -> Sigma [b : B] R a b)</div><div> -> Sigma [f : A -> B] ((a : A) -> R a b)</div><div>ac f = (fst o f, snd o f)</div><div><br></div><div>In Type Theory this principle is provable because the premise already gives us a function producing tuples and all we need to do is to compose with the projections. However, this version of the axiom of choice relies essentially on the type-theoretic idea that not just the existence of a proof matters but also the particular choice of proofs. That is our constructions lives in Set not in Prop. If we try to reconstruct the axiom of choice as we know it from predicate logic we have to restrict ourselves to Prop. Clearly it is Sigma which gets us out of Prop, because Sigma [b : B] R a b : Set even though R a b: Prop. In contrast (b : B) -> R a b : Prop. We can fix this by using an operation A* : Prop where A : Set which I would call "inhabited" (while Awodey and Bauer call it bracket types). That is we define Exists A P = (Sigma A P)* where Exists A P : Prop if P : A -> Prop even though A : Set. We can now state the propositional axiom of choice:</div><div><br></div><div>pac : ((a : A) -> Exists [b : B] R a b)</div><div> -> Exists [f : A -> B] ((a : A) -> R a b)</div><div> </div><div>Now pac is not provable (in Type Theory with Prop and *) because it clearly is a lie. In the premise I am hiding the choice of B but in the conclusion I am allowed to peek into this hidden result to construct a function. One may think that it is ok because I am also hiding the illegitimate function constructed. However, this is not so because I can still derive propositional consequences of the function constructed. And as Diaconescu shows one of the consequences is the excluded middle (for any P : Prop). </div><div><br></div><div>When translating Diconescu's construction into Type Theory we are using a quotient type for A. It turns out that this is essential and that pac is actually harmless in the absence of quotient types (this can be shown using the setoid model). </div><div><br></div><div>My conclusion is that if you do constructive reasoning you should use Type Theory instead of predicate logic because the proofs matter and it is just misleading to restrict yourselves to Prop.</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div><div>P.S. Sorry for no having formalized this in Agda yet… I guess I have to postulate quotient types.</div><div><br></div><span id="OLK_SRC_BODY_SECTION"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Liang-Ting Chen <<a href="mailto:L.Chen@cs.bham.ac.uk">L.Chen@cs.bham.ac.uk</a>><br><span style="font-weight:bold">Date: </span> Tue, 20 Nov 2012 23:42:40 +0000<br><span style="font-weight:bold">To: </span> "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> Re: [Agda] Re: Classical Mathematics for a Constructive World<br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><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></blockquote></span>
<br><br>
<br></body></html>