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
3
votes
1
answer
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
1
answer
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 ...
- 619
2
votes
1
answer
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 ...
- 9,653
3
votes
1
answer
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 ...
- 9,931
7
votes
1
answer
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 ...
5
votes
1
answer
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 ...
- 9,931
16
votes
3
answers
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. \...
- 2,868
9
votes
1
answer
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 ...
- 2,353
18
votes
3
answers
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 ...
JNat♦
- 101