# 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, ...
• 161
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 ...
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 ...
• 233
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 ...
• 9,653
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. \...
627 views

### What axioms do I need to search the naturals?

Theorem search {P : nat -> Prop} (dec : forall n, {P n} + {~P n}) : ~~(exists n, P n) -> {n | P n}. Admitted. I don't think this is provable in Coq without ...
• 573
1k views

### Well-foundedness: classical equivalence of no infinite descent and accessibility

I have often seen the claim that in a classical setting, well-foundedness of a relation > defined as the absence of an infinite descent ...