[Agda] Re: Agda Digest, Vol 87, Issue 24

Wed Nov 21 12:04:05 CET 2012

hey Martin,

this is too cryptic for me:

*The so-called "Curry-Howard isomorphism" seems to say that exists-forall
are the same as Sigma-Pi. They are not the same. In fact, homotopy type
theory, if you are following this recent trend, is re-introducing the
distinction in a constructive context, and even at a syntactic,
model-independent, level.
*
Can you elaborate, please?

Thank you Liang-Ting Chen for the info  about the existence of
 Martin-Loef's paper.

best,
Valeria

>
> Message: 5
> Date: Wed, 21 Nov 2012 01:09:51 +0000
> From: Martin Escardo <m.escardo at cs.bham.ac.uk>
> Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World
> To: Liang-Ting Chen <L.Chen at cs.bham.ac.uk>
> Cc: agda at lists.chalmers.se
> Message-ID: <50AC29DF.5060308 at cs.bham.ac.uk>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> On 20/11/12 23:42, Liang-Ting Chen wrote:
>
> > 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?,
>
> Good that you mentioned that.
>
> Let me then add more fuel to the general heated confusion about choice,
> and then try to clarify the situation.
>
> In most toposes, the axiom of choice fails, simply because in any topos
> choice implies excluded middle, as toposes are mathematical models of
> intuitionistic set theory. And typically toposes fail badly regarding
> the validation of excluded middle, in trivial ways, even in the examples
> of toposes that have nothing to do with constructive mathematics.
>
> Yet, any topos, being locally cartesian closed, is a model of Martin-Lof
> type theory, in which choice is a theorem. How come?
>
> Contradiction. (?)
>
> Of course not. In a topos, one has "exists" and "forall", and also
> "Sigma" and "Pi". Choice fails often when formulated for exists-forall,
> but always holds when formulated for Sigma-Pi.
>
> One can say, loosely speaking: Any topos satisfies "Martin-Lof" choice,
> but hardly any topos satisfies "Set-theoretical" choice.
>
> The so-called "Curry-Howard isomorphism" seems to say that exists-forall
> are the same as Sigma-Pi. They are not the same. In fact, homotopy type
> theory, if you are following this recent trend, is re-introducing the
> distinction in a constructive context, and even at a syntactic,
> model-independent, level.
>
> In summary, choice may fail in its exists-forall formulation, but it
> always holds in its Sigma-Pi formulation (and rather trivially in both
> cases).
>
> I hope this is not too cryptic.
>
> Best,
> Martin
>
>
>
>
>
> ------------------------------
>
> Message: 6
> Date: Wed, 21 Nov 2012 09:46:52 +0000
> From: Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk>
> Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World
> To: Liang-Ting Chen <L.Chen at cs.bham.ac.uk>, "agda at lists.chalmers.se"
>         <agda at lists.chalmers.se>
> Message-ID: <CCD24D62.A3508%psztxa at exmail.nottingham.ac.uk>
> Content-Type: text/plain; charset="windows-1252"
>
> Hi,
>
> 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?):
>
> ac : ((a : A) -> Sigma [b : B] R a b)
>     -> Sigma [f : A -> B] ((a : A) -> R a b)
> ac f = (fst o f, snd o f)
>
> 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:
>
> pac : ((a : A) -> Exists [b : B] R a b)
>     -> Exists [f : A -> B] ((a : A) -> R a b)
>
> 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).
>
> 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).
>
> 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.
>
> Cheers,
> Thorsten
>
> P.S. Sorry for no having formalized this in Agda yet… I guess I have to
> postulate quotient types.
>
> From: Liang-Ting Chen <L.Chen at cs.bham.ac.uk<mailto:L.Chen at cs.bham.ac.uk>>
> Date: Tue, 20 Nov 2012 23:42:40 +0000
> To: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <
> agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
> Subject: Re: [Agda] Re: Classical Mathematics for a Constructive World
>
>
>
> On 20 November 2012 13:28, Martin Escardo <m.escardo at cs.bham.ac.uk<mailto:
> 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
>
> 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.
> 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
>
>
> End of Agda Digest, Vol 87, Issue 24
> ************************************
>

-- 
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121121/ac1d9837/attachment.html