If I type `Require Import Classical.`

I get to work in a context with excluded middle, and many of its consequences have already been added. Is there an equivalent module to import to have both excluded-middle and axiom of choice?

Answering my own question here: I had not explored enough, and it seems that when type `Require Import Classical`

one does have the axiom of choice on bord, under the name `Choice`

. So my question does look a little stupid.

Well, no, I got it wrong with `Choice`

. This definition is constructive, and so it is much weaker than classical choice. Now, I think the good answer was `Require Import ClassicalChoice.`

and then use `choice`

.

Shouldn't this knowledge be part of the FAQ, for instance extending this item to explain how to get access to axioms defined in the stdlib in practice ? I have the feeling that this kind of questions are frequently asked on SO.

I agree, I will look at the item you are pointing too. My only difficulty is that going to the FAQ is not natural to me. Incidentally, I don't know if it is natural to anybody.

My experience suggests that most mathematicians have the unexamined assumption that there is something intrinsically nonconstructive about AC. I think this is because we associate it with the Banach-Tarski paradox. But if you look at AC and squint, you notice that it fits just fine into the constructive view. Bishop commented on this in one of his books, probably *Constructive Analysis* but I cannot find the citation.

I guess it depends on what you mean by constructive. You can prove LEM using AC so I would call AC non-constructive

This depends a lot on how extensional AC is formulated. AC + predicate extensionality yields Excluded Middle: https://coq.inria.fr/library/Coq.Logic.Diaconescu.html

The related Bishop quote is "A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence." and its indeed from Constructive Analysis. Wikipedia also has some words on the matter: https://en.wikipedia.org/wiki/Axiom_of_choice#In_constructive_mathematics

ZF is too coarse to make really sense of that. I think that Bishop's claim is tantamount to dependent elimination for Σ-types.

... which is built-in in CIC.

even functional choice expressed as the commutation of Prop-squashing with Π can be considered constructive.

So I believe that any debate about AC is bound to generate confusion if you don't explain what system you're working in and what version of AC you consider.

@Ali Caglayan's comment is pretty much an instance of confusion-inducing statement. AC does not imply EM per se, as explained by @Yannick Forster you need a strong extensionality principle in addition to AC alone.

Worse, constructivity is not well defined. I'd even go as far as saying that EM ** on Prop** is still constructive.

Pierre-Marie Pédrot said:

Worse, constructivity is not well defined. I'd even go as far as saying that EM

is still constructive.on Prop

"Meaningful distinctions deserve to be maintained." :smile:

I agree with @Pierre-Marie Pédrot that what I wrote can be interpreted differently by others. To be clear, if you have MLTT with hprop-truncations then you can write down a statement of AC. This should have nothing to do with sigma-elimination (which I hear sometimes gets called the type-theoretic AC). The statement of AC that I have in mind basically says that hprop-truncations "commute" with pi-types. Then the satement of LEM should be any hprop is decidable. From that, what I said above becomes correct in that AC => LEM.

I am fairly sure you still need propext + funext for this to hold.

(I mean, at least enough extensionality to prove predicate extensionality.)

Yes, I think funext would suffice, but I wouldn't say this is non-constructive tho

I believe that the real issue is that funext + functional AC is deeply non-constructive.

There is no way to pick a representative function out of an extensional description of its squashed input graph.

In fact, hprop-truncation is enough to give funext

Depends how you phrase it.

As a HIT with full dependent eliminator it should suffice

you can define an "interval" type as the truncation of bool

and from that derive funext

Hm, right.

Last updated: Oct 03 2023 at 21:01 UTC