hey Martin,<div><br></div><div>this is too cryptic for me:</div><div><br></div><div><i><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">The so-called "Curry-Howard isomorphism" seems to say that exists-forall</span><br style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">
<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">are the same as Sigma-Pi. They are not the same. In fact, homotopy type</span><br style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">
<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">theory, if you are following this recent trend, is re-introducing the</span><br style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">
<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">distinction in a constructive context, and even at a syntactic,</span><br style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">
<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.800000190734863px;background-color:rgb(255,255,255)">model-independent, level.</span><br></i><br>Can you elaborate, please?</div><div><br></div><div>
Thank you Liang-Ting Chen for the info about the existence of Martin-Loef's paper.</div><div><br></div><div>best,</div><div>Valeria</div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Message: 5<br>
Date: Wed, 21 Nov 2012 01:09:51 +0000<br>
From: Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>><br>
Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World<br>
To: Liang-Ting Chen <<a href="mailto:L.Chen@cs.bham.ac.uk">L.Chen@cs.bham.ac.uk</a>><br>
Cc: <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
Message-ID: <<a href="mailto:50AC29DF.5060308@cs.bham.ac.uk">50AC29DF.5060308@cs.bham.ac.uk</a>><br>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed<br>
<br>
On 20/11/12 23:42, Liang-Ting Chen wrote:<br>
<br>
> After Martin's reply, I just want to mention the following article by<br>
> Per Martin-Löf which explains that the "extensional" choice / Zermelo's<br>
> choice imply excluded middle in MLTT:<br>
><br>
> Martin-Lof, 100 years of Zermelo's axiom of choice: what was the problem<br>
> with it?,<br>
<br>
Good that you mentioned that.<br>
<br>
Let me then add more fuel to the general heated confusion about choice,<br>
and then try to clarify the situation.<br>
<br>
In most toposes, the axiom of choice fails, simply because in any topos<br>
choice implies excluded middle, as toposes are mathematical models of<br>
intuitionistic set theory. And typically toposes fail badly regarding<br>
the validation of excluded middle, in trivial ways, even in the examples<br>
of toposes that have nothing to do with constructive mathematics.<br>
<br>
Yet, any topos, being locally cartesian closed, is a model of Martin-Lof<br>
type theory, in which choice is a theorem. How come?<br>
<br>
Contradiction. (?)<br>
<br>
Of course not. In a topos, one has "exists" and "forall", and also<br>
"Sigma" and "Pi". Choice fails often when formulated for exists-forall,<br>
but always holds when formulated for Sigma-Pi.<br>
<br>
One can say, loosely speaking: Any topos satisfies "Martin-Lof" choice,<br>
but hardly any topos satisfies "Set-theoretical" choice.<br>
<br>
The so-called "Curry-Howard isomorphism" seems to say that exists-forall<br>
are the same as Sigma-Pi. They are not the same. In fact, homotopy type<br>
theory, if you are following this recent trend, is re-introducing the<br>
distinction in a constructive context, and even at a syntactic,<br>
model-independent, level.<br>
<br>
In summary, choice may fail in its exists-forall formulation, but it<br>
always holds in its Sigma-Pi formulation (and rather trivially in both<br>
cases).<br>
<br>
I hope this is not too cryptic.<br>
<br>
Best,<br>
Martin<br>
<br>
<br>
<br>
<br>
<br>
------------------------------<br>
<br>
Message: 6<br>
Date: Wed, 21 Nov 2012 09:46:52 +0000<br>
From: Altenkirch Thorsten <<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>><br>
Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World<br>
To: Liang-Ting Chen <<a href="mailto:L.Chen@cs.bham.ac.uk">L.Chen@cs.bham.ac.uk</a>>, "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>"<br>
<<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
Message-ID: <<a href="mailto:CCD24D62.A3508%25psztxa@exmail.nottingham.ac.uk">CCD24D62.A3508%psztxa@exmail.nottingham.ac.uk</a>><br>
Content-Type: text/plain; charset="windows-1252"<br>
<br>
Hi,<br>
<br>
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?):<br>
<br>
ac : ((a : A) -> Sigma [b : B] R a b)<br>
-> Sigma [f : A -> B] ((a : A) -> R a b)<br>
ac f = (fst o f, snd o f)<br>
<br>
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:<br>
<br>
pac : ((a : A) -> Exists [b : B] R a b)<br>
-> Exists [f : A -> B] ((a : A) -> R a b)<br>
<br>
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).<br>
<br>
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).<br>
<br>
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.<br>
<br>
Cheers,<br>
Thorsten<br>
<br>
P.S. Sorry for no having formalized this in Agda yet… I guess I have to postulate quotient types.<br>
<br>
From: Liang-Ting Chen <<a href="mailto:L.Chen@cs.bham.ac.uk">L.Chen@cs.bham.ac.uk</a><mailto:<a href="mailto:L.Chen@cs.bham.ac.uk">L.Chen@cs.bham.ac.uk</a>>><br>
Date: Tue, 20 Nov 2012 23:42:40 +0000<br>
To: "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><mailto:<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><mailto:<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>>><br>
Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World<br>
<br>
<br>
<br>
On 20 November 2012 13:28, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a><mailto:<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>>> wrote:<br>
On 20/11/12 12:03, Jan Burse wrote:<br>
Diaconescu's Theorem<br>
<a href="http://en.wikipedia.org/wiki/Diaconescu%27s_theorem" target="_blank">http://en.wikipedia.org/wiki/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>
<br>
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/entries/mathematics-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>
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:<br>
<br>
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" target="_blank">http://comjnl.oxfordjournals.org/content/49/3/345.extract</a><br>
<br>
<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<br><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
End of Agda Digest, Vol 87, Issue 24<br>
************************************<br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br>Valeria de Paiva<br><a href="http://www.cs.bham.ac.uk/~vdp/" target="_blank">http://www.cs.bham.ac.uk/~vdp/</a><br><a href="http://valeriadepaiva.org/" target="_blank">http://valeriadepaiva.org/</a><br>
</div>