Questions tagged [axiom-of-choice]

An important and fundamental axiom in set theory sometimes called Zermelo's axiom of choice. It was formulated by Zermelo in 1904 and states that, given any set of mutually disjoint nonempty sets, there exists at least one set that contains exactly one element in common with each of the nonempty sets. The axiom of choice is related to the first of Hilbert's problems. (from MathOverflow)

9 questions
Filter by
Sorted by
Tagged with
289 views

Determining why my proof depends on the axiom of choice

I would like to write constructive proofs in Lean 4, so I don't want my proofs to depend on Classical.choice, the axiom of choice. However, one of my proofs does, ...
1 vote
112 views

Proving function existence in Coq

Coq beginner here! My question is how to formalize reasoning of the kind "...consider the following function, it has some property, therefore..." in Coq. The challenge is to prove the ...
326 views

Eliminating "Exists Unique" in Lean 3

In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element ...
156 views

Partial and multi-valued choice principles/description operators

I have a hunch I need to figure out versions of unique choice or definite description for partial and multi-valued functions. But I'm entirely confused about how you'd axiomize partial or multi-valued ...
544 views

How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?

Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global ...
325 views

Does one need a type-theoretical axiom of choice for singletons?

In Zermelo-Fraenkel axiomatics, one does not need to use the axiom of choice to resolve unique existential quantifiers, the axiom of replacement is enough for this. But it seems that Type theory does ...
1k views

Do you need a Hilbert style Epsilon operator for definitions in set theory?

I've started to play with mechanizing some set theory stuff. I'm not sure if I want a constructive flavor or not yet. Anyhow you can do stuff like axiomize the empty set  \top \vdash \exists P. \...