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
14 votes
3 answers
719 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. \...
user avatar
9 votes
1 answer
531 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 ...
user avatar
  • 303
16 votes
3 answers
835 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 ...
user avatar