[Agda] Re: Classical Mathematics for a Constructive World

[Altenkirch Thorsten]

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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



--
Liang-Ting Chen, PhD student
School of Computer Science,
The University of Birmingham, UK


This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.



This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121121/3bdcafef/attachment-0001.html