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)

Filter by
Sorted by
Tagged with
18 votes
2 answers
334 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., ...
KANG Rongji's user avatar