nLab countable set

Countable sets


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Countable sets


Let SS be any set, and let N\mathbf{N} be the set of natural numbers. Let |S||S| be the cardinality of SS, and let 0\aleph_0 be the cardinality of N\mathbf{N}.

Then SS is:

  • denumerable if |S|= 0{|S|} = \aleph_0,
  • countable if |S| 0{|S|} \leq \aleph_0, and
  • uncountable if |S|> 0{|S|} \gt \aleph_0.

Note that the first two terms are not entirely standardised; some authors use them interchangeably for one or the other concept.


If you accept the axiom of choice, then there is really nothing more to say than what was above. In weaker foundations, more care may be needed. The following definitions should be more than enough for practical use in constructive mathematics:

  • A set SS is denumerable if there exists a bijection between SS and N\mathbf{N}; or in other words if SS is the same as N\mathbf{N} up to isomorphism? in Set.
  • SS is denumerably indexed if there exists a surjection to SS from N\mathbf{N} (or equivalently any denumerable set); or in other words if SS a quotient set of a N\mathbf{N}, up to isomorphism.
  • SS is countable if there exists a bijection between SS and a detachable lower subset of N\mathbf{N}.
  • SS is countably indexed if there exists a surjection to SS from a countable set.
  • SS is subcountable (or subdenumerable) if there exists an injection from SS to a countable set, or equivalently to a denumerable set; or in other words if SS is a subset of N\mathbf{N}, up to isomorphism.
  • SS is subcountably indexed (or subdenumerably indexed) if SS is a subquotient of N\mathbf{N}, up to isomorphism.
  • SS is uncountable if, given any function ff from a detachable subset of N\mathbf{N} to SS, the function is strongly non-surjective in the sense that there exists an element of SS that is not in the image of ff.

Of course, the terms are even less standardised here. Certainly it is common for ‘countable’ to mean countably indexed, and yet it may also (as in classical mathematics) mean denumerable. In at least some contexts, ‘enumerable’ (without the initial ‘d’) means denumerably indexed.

Not only does the difference between ‘denumerable’ and ‘countable’ disappear when we add the prefix ‘sub’ (for obvious reasons), but it almost disappears when we add the suffix ‘ly indexed’! Specifically, a set is denumerably indexed if and only if it is both inhabited and countably indexed; and a set is countably indexed if and only if it is either empty or denumerably indexed. That countability involves lower subsets of \mathbb{N} is also almost irrelevant here; any inhabited detachable subset of \mathbb{N} is denumerably indexed regardless of its closure under order.

On the other hand, it is key that countability involves detachable subsets of \mathbb{N}, so that not every subcountable set is necessarily countable (or even countably indexed). Indeed, the set of computable numbers is subcountably indexed, while the set of real numbers is uncountable (and thus not countably indexed); yet in Russian constructivism, these are the same set! One reason to focus on countably indexed sets is that this is about the most general concept that definitely does not hold of the set of real numbers.

There is a lot of freedom in defining uncountability. You can start with countable or countably indexed sets and require that any function from them to SS be non-surjective (in the strong sense used in the definition above). Or you can start with denumerable or denumerably indexed sets and require that any function from them to SS be non-surjective, then add the additional clause that SS must be inhabited. Or you can compromise, and start with a detachable subset of \mathbb{N} without requiring it to be a lower subset, since this is enough to prove SS inhabited and make the order-closure irrelevant. All of these definitions are equivalent!

Arguably, uncountability is really a property of a set equipped with? an inequality relation #\#. Then SS is #\#-uncountable, or the pair (S,#)(S,\#) is strongly uncountable (or just uncountable if context is clear) if, given any function ff from a detachable subset of N\mathbf{N} to SS (or equivalently any variation as in the previous paragraph), the function is #\#-strongly non-surjective in the sense that there exists an element of SS that is #\#-distinct from every element in the image of ff. Then the mere set SS is uncountable if and only if it is uncountable when equipped with the denial inequality.

Examples and Properties

The set of real numbers is uncountable. Even in constructive mathematics, this is true for pretty much any notion of real number, from regular Cauchy real numbers to MacNeille real numbers, by any of the usual arguments.

Every denumerable set is infinite, and hence so is every set with a denumerable subset. Classically (usng dependent choice DCDC), we have the converse: a set is infinite if and only if it has a denumerable subset. If a set has a denumerable subset, then its power set is uncountable. Even without DCDC, using excluded middle instead, the power set of an infinite set is uncountable.

In contrast, the set of algebraic numbers is denumerable. Also, the set of computable numbers is subcountably indexed (and infinite, so denumerable in classical mathematics). Combined with the uncountability of the real numbers, this gives the existence of transcendental numbers (constructively) and uncomputable numbers (classically).

Classically, every set is countable xor uncountable. Even constructively, a countably indexed set cannot be uncountable. In Russian constructivism, however, there are subcountable sets that are also uncountable. In particular, the set of computable numbers is subcountably indexed, while the set of real numbers is uncountable, yet in Russian constructivism, these are the same set! In some formalisms of Russian constructivism, every set is subcountably indexed.

The empty set is countable, although not denumerably indexed. Conversely, any uncountable set must be inhabited, as must be any denumerably indexed set. Even constructively, a countable set is empty xor inhabited.

Every finite set is countable, every finitely indexed set is countably indexed, every subfinite set is subcountable, and every subfinitely indexed set is subcountably indexed. Conversely, every uncountable set is infinite.

Classically, a denumerable set is precisely an infinite countable set; sometimes this is written as a countably infinite set. Thus classically, a countable set is finite xor denumerable. Even constructively, a countable set is denumerable if and only if it is not finite.

Classically (using countable choice), countable unions of countable sets are countable.


Arguably, set theory as such begins with the 1873 correspondence between Georg Cantor and Richard Dedekind on countability. Although they tacitly used excluded middle throughout, generally speaking, their results were constructive if taken to be about countably indexed sets. They worked out the countability of the algebraic numbers and the uncountability of the real numbers, including both constructive and nonconstructive proofs of the existence of transcendental numbers. (This was the same year that Charles Hermite published a proof that e\mathrm{e} is transcendental, although Joseph Liouville had shown how to artificially construct transcendental numbers as early as 1851.)

In subsequent correspondence with Cantor, Karl Weierstrass stressed the usefulness of the countability of the algebraic numbers but downplayed the notion of uncountability. Still, he urged Cantor to publish. Since Weierstrass and the finitist Leopold Kronecker were senior editors at Krelle's Journal, Cantor wrote his 1874 article carefully. He showed the denumerability of the algebraic numbers explicitly and titled the article as if that were the only subject. He then added a footnote in the proofreading stages, using an interval-based argument, showing how a transcendental number could be constructed from this denumeration.

Cantor's argument was essentially a constructive proof that the set of real numbers is uncountable, as it could apply to any denumerably indexed subset. He tacitly used LLPO, but it's straightforward to avoid this using binary meets and joins of real numbers, which are constructive. He also used a Dedekind cut to construct the final transcendental number, and it is this that Kronecker would have most likely objected to, since it is an irreducibly infinite procedure to construct a single number. However, the argument is acceptable to any non-finitist constructivist.

In the correspondence with Dedekind, it was Cantor who first considered and proved the uncountability of the real numbers but Dedekind who first considered and proved the countability of the algebraic numbers, which was the ostensible subject of Cantor's article. Furthermore, it was Dedekind who first wrote the interval-based proof that Cantor used in his footnote that was the real point of the article. However, Cantor gave Dedekind no credit. This strained their relationship for a few years afterward.

The diagonal argument also shows the uncountability of the real numbers (nonconstructively through Cantor's Theorem on the cardinality of power sets, constructively through a slight generalization), but Cantor did not publish this until 1891. Interpreted finitistically as an algorithm to construct, from a sequence of real numbers, an approximation of a hypothetical number not in the sequence, the diagonal argument is more efficient; pedagogically, it is easier to explain. However, it was not the first.


which discusses both the origin of the 1874 article and the questions of constructivity that arose in its aftermath.

Last revised on August 10, 2023 at 13:00:13. See the history of this page for a list of all contributions to it.