Questions tagged [countable-choice]
The axiom of countable choice (CC), also called ACω or ACN, is a weak form of the axiom of choice; it says that the set of natural numbers is a projective object in Set. (Recall that the full axiom of choice states that every set is projective.) (from nLab)
1
question
17
votes
2
answers
287
views
Is there computational interpretation for countable choice?
I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., ...
- 660