Axiom of choice for sets

Stream: Is there code for X?

[Terence Tao]

I recently needed a choice function for existential statements restricted to sets, to wit:

noncomputable def Set.choose {α: Type} {S: Set α} {P: α → Prop} (h: ∃ s ∈ S, P s) : S :=
  {
    val := Classical.choose h
    property := (Classical.choose_spec h).1
  }

lemma Set.choose_spec {α: Type} {S: Set α} {P: α → Prop} (h: ∃ s ∈ S, P s) : P (Set.choose h) := (Classical.choose_spec h).2

Are these already in Mathlib by some other name? Or is the use of sets as subtypes discouraged?

[Aaron Liu]

Is docs#Exists.choose not good enough?

[Jireh Loreaux]

Exists.choose doesn't work for bounded existential quantifiers like Terry has here.

[Riccardo Brasca]

There is nothing wrong with the definition, but in practice it is ⟨_, (Classical.choose_spec h).1⟩. I would use it as an abbrev or something very reducible, since otherwise it is just a barrier to use all the existing library about choose and choose_spec.

[Jireh Loreaux]

You can also just rewrite your existential as over the subtype:

example {X : Type*} {s : Set X} {p : X → Prop} : (∃ x ∈ s, p x) ↔ ∃ x : s, p x := by
  simp only [Subtype.exists, exists_prop]

then you can use docs#Exists.choose as Aaron indicated.

[Jireh Loreaux]

This would be my approach unless you need to have it repeatedly. And if that is the case, it would at least make me question whether there's a better way by avoiding subtypes (but perhaps there isn't).

[Jireh Loreaux]

Note that if we had Set.choose, there would be no reason not to have Finset.choose too. :face_with_diagonal_mouth:

[Terence Tao]

In my application, α is a Preorder but s IsDirected, and I need tools that only work on directed types (in particular, I want to use Filter.atTop (α := s), which only behaves as I want because IsDirected s), so I wanted to work with the subtype s at least some of the time; on the other hand, many of my other tools most naturally live in α, in particular it is slightly more natural to quantify over x ∈ s rather than x:s. I guess I could refactor more things to live in s rather than α and rely on the implicit type conversion, but I had the impression that the Mathlib style was to prefer to minimize the use of subtypes

[Aaron Liu]

Jireh Loreaux said:

Note that if we had Set.choose, there would be no reason not to have Finset.choose too. :face_with_diagonal_mouth:

We already have docs#Finset.choose, which is unique choice for finsets

[Jireh Loreaux]

Just noting that we have docs#DirectedOn, although it doesn't solve your issue.

[Jireh Loreaux]

You're not working with approximate identities in some function space, perchance, are you? Either way, you might have a look at some work I did in a similar situation when I developed the canonical approximate identity in a C⋆-algebra: see docs#CStarAlgebra.directedOn_nonneg_ball and the rest of that file.

[Jireh Loreaux]

Terry, the other possibility if you work with the subset s enough as a subtype is to give it an actual def, especially if it has properties beyond IsDirected. Then you can set up enough API that it's not so painful to go back and forth between s and α, and you don't have to feel bad about doing so.

[Terence Tao]

The code is at equational#1135. The task is basically completed and I should have no further need of directed sets in the rest of the project, so I'm happy with it as is (I made the one change of turning Set.choose into an abbrev, though.)

[Terence Tao]

There was a separate minor issue actually in that there wasn't quite a lemma to turn IsChain into IsDirected so I had to add that as well by gluing together three or four existing lemmas.

[Mario Carneiro]

Riccardo Brasca said:

There is nothing wrong with the definition, but in practice it is ⟨_, (Classical.choose_spec h).1⟩. I would use it as an abbrev or something very reducible, since otherwise it is just a barrier to use all the existing library about choose and choose_spec.

I'm not sure there is much "all the existing library about choose and choose_spec", in fact I think you just listed the entire library right there, those two functions. This is kind of the point of the axiom of choice, you know literally nothing other than the choose_spec lemma

[Mario Carneiro]

it's not a huge burden to have a few variations on the interface with their own two functions

[Mario Carneiro]

we already have docs#Classical.choice, docs#Classical.epsilon, docs#Classical.indefiniteDescription, docs#Classical.choose, docs#Exists.choose

[Edward van de Meent]

and of course docs#zorn_subset and friends

[Mario Carneiro]

that one's actually not a function though, interestingly enough

[Edward van de Meent]

ah, you're right

[Mario Carneiro]

if it's a theorem then you really only need the one theorem in order to provide the complete API, for global choice principles you need the function and its axiom

[Mario Carneiro]

unless the function has a dependent enough type like Classical.indefiniteDescription that no additional theorem is needed

[Edward van de Meent]

Mario Carneiro said:

that one's actually not a function though, interestingly enough

btw, am i right that this means that mathlib's zorn's lemma does not imply mathlib's choice?

[Mario Carneiro]

that is correct

[Edward van de Meent]

curious

[Mario Carneiro]

mathlib uses an axiom called "global choice" in the set theory literature, which is stronger than choice

[Mario Carneiro]

The equivalent statement in ZFC would be "there is a proper class well ordering function on the universe"

[Mario Carneiro]

it means that anything choicy becomes not merely existing but definable

[Mario Carneiro]

with ZFC alone it is still the case that there is no definable well order of the reals

[Mario Carneiro]

They are very closely related though, and in particular they are equiconsistent. In a world where lean only assumed Nonempty (∀A, Nonempty A -> A) which is equivalent to the (weak) axiom of choice, you could have a nullary typeclass [Choicy.{u}] defined as ∀A : Sort u, Nonempty A -> A and use it to define things as we normally do, and then you can discharge this assumption once you get to the "end", if it's a theorem you wanted to prove

[Edward van de Meent]

is there a version of zorn's lemma that's equivalent to global choice though? i.e. is it just a quirk of mathlib's formulation that they're not equivalent?

[Mario Carneiro]

zorn's lemma is supposed to be equivalent to the axiom of choice, not global choice

[Mario Carneiro]

if you wanted something equivalent to global choice then you need global zorn

[Mario Carneiro]

just replacing the existential quantifier with a subtype should do the trick

[Mario Carneiro]

another fun fact: HoTT is consistent with the axiom of choice, but inconsistent with global choice

[Edward van de Meent]

iirc, similarly, global choice is consistent with weak univalence but not actual univalence?

[Edward van de Meent]

don't quote me on that tho

[Mario Carneiro]

I've never heard of weak univalence before, do you know where you heard about it?

[Edward van de Meent]

either on this zulip or on the lean discord (not xena)

[Edward van de Meent]

i seem to recall it's Equiv a b -> a = b?

[Mario Carneiro]

I think that one is consistent with lean, it forces the cardinality model though which is a bit weird

[Edward van de Meent]

i think Bhavik Mehta was the one who mentioned it on the discord, they likely will know more

[Mario Carneiro]

he won't hear you unless you speak up: @Bhavik Mehta

[Edward van de Meent]

i know, but i thought that since this is kinda off-topic, if you wanted to know more, you could dm him instead of polluting the thread

[Edward van de Meent]

and if you are satisfied, no need to ping him

[Kevin Buzzard]

He's busy dealing with 30 incoming final Lean projects for his (formerly my) course :-)

[Jz Pan]

Jireh Loreaux said:

Note that if we had Set.choose, there would be no reason not to have Finset.choose too. :face_with_diagonal_mouth:

Finset.choose does not need the axiom of choice and is a computable def (but need DecidablePred P instead), since by definition one can enumerate elements of a Finset and check that if P is satisfied for them.

[Bhavik Mehta]

My recollection is that Equiv a b -> a = b, together with Quot.sound, implies global choice (and hence LEM), which Chris H told me about: https://gist.github.com/ChrisHughes24/730522373e1d95cbcf961625af5b8eab. I agree with Mario that it should be consistent and forces the cardinality model

[Jireh Loreaux]

Jz Pan said:

Finset.choose does not need the axiom of choice and is a computable def

When I made this comment, I was referring not to the existing docs#Finset.choose (which takes a unique existential), but the analogue of docs#Exists.choose and Set.choose which would simply take a bounded existential.