Stream: Coq users

Topic: Work in classical logic with Axiom of Choice


view this post on Zulip Yves Bertot (Jun 25 2021 at 06:37):

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?

view this post on Zulip Yves Bertot (Jun 25 2021 at 06:46):

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.

view this post on Zulip Yves Bertot (Jun 25 2021 at 07:07):

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.

view this post on Zulip Kenji Maillard (Jun 25 2021 at 07:33):

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.

view this post on Zulip Yves Bertot (Jun 25 2021 at 12:25):

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.

view this post on Zulip Martin Harrison (Jun 27 2021 at 11:56):

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.

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:04):

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

view this post on Zulip Yannick Forster (Jun 27 2021 at 12:05):

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

view this post on Zulip Yannick Forster (Jun 27 2021 at 12:06):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:06):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:07):

... which is built-in in CIC.

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:08):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:09):

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.

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:09):

@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.

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:11):

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

view this post on Zulip Martin Harrison (Jun 27 2021 at 12:12):

Pierre-Marie Pédrot said:

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

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

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:23):

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.

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:24):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:24):

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

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:27):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:28):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:28):

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

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:29):

In fact, hprop-truncation is enough to give funext

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:30):

Depends how you phrase it.

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:30):

As a HIT with full dependent eliminator it should suffice

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:30):

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

view this post on Zulip Ali Caglayan (Jun 27 2021 at 12:30):

and from that derive funext

view this post on Zulip Pierre-Marie Pédrot (Jun 27 2021 at 12:31):

Hm, right.


Last updated: Feb 01 2023 at 13:03 UTC