Skip to main content

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)

Filter by
Sorted by
Tagged with
3 votes
1 answer

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, ...
Robin Green's user avatar
1 vote
1 answer

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 ...
userl6kgPo0ixv's user avatar
2 votes
1 answer

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 ...
Zongshu Wu's user avatar
3 votes
1 answer

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 ...
Ms. Molly Stewart-Gallus's user avatar
5 votes
1 answer

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 ...
ACL's user avatar
  • 233
6 votes
1 answer

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 ...
Jason Rute's user avatar
  • 8,685
16 votes
3 answers

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. \...
Ms. Molly Stewart-Gallus's user avatar
9 votes
1 answer

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 ...
HTNW's user avatar
  • 533
16 votes
3 answers

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 ...
Théo Winterhalter's user avatar