[Agda] Re: Classical Mathematics for a Constructive World
Martin Escardo
m.escardo at cs.bham.ac.uk
Wed Nov 21 02:09:51 CET 2012
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
More information about the Agda
mailing list