nLab countable set

Countable sets

Context

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
propositionsetobjecttype
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

semantics

Countable sets

Idea

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.

Definitions

Countable sets

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 constructively denumerable if it comes with the structure of a bijection between SS and N\mathbf{N}.
  • 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 split denumerably indexed if there exists a split surjection to SS from N\mathbf{N}.
  • SS is constructively denumerably indexed or constructively split denumerably indexed if it comes with the structure of a surjection to SS from N\mathbf{N} and a section of said surjection.
  • SS is countable if there exists a bijection between SS and a detachable lower subset of N\mathbf{N}.
  • SS is constructively denumerable if it comes with the structure of 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 split countably indexed if there exists a split surjection to SS from a countable set.
  • SS is constructively countably indexed or constructively split countably indexed if it comes with the structure of a surjection to SS from a countable set and a section of said surjection.
  • 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 constructively subcountable (or constructively subdenumerable) if it comes with the structure of an injection from SS to a countable set, or equivalently to a denumerable set.
  • SS is subcountably indexed (or subdenumerably indexed) if SS is a subquotient of N\mathbf{N}, up to isomorphism.
  • SS is split subcountably indexed (or split subdenumerably indexed) if there exists a split surjection to SS from a subcountable set, or equivalently if there exists an injection from SS to a split countably indexed set or equivalently to a split denumerably indexed set.
  • SS is BHK-subcountably indexed or BHK-split subcountably indexed if it comes with the structure of a surjection to SS from a subcountable set and a section of said surjection.

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! Furthermore, Andrej Bauer and James Hanson have showed that there is a topos in which the Dedekind real numbers are countably indexed, which they refer to as “countable” in their paper.

One reason to focus on subcountable sets is that this is about the most general concept that definitely does not hold of the set of real numbers. Every split countably indexed set AA is subcountable due to there existing a injective section for the surjection from the detachable subset of \mathbb{N} into AA.

In addition, in the presence of countable choice, the difference between denumerably indexed and split denumerably indexed, countably indexed and split countably indexed, and subcountably indexed and split subcountably indexed disappear, since every surjection out of \mathbb{N} and every subset of \mathbb{N} has a section by countable choice.

Under the BHK interpretation of constructive mathematics, one only has the BHK versions of denumerably indexed, countably indexed, subcountably indexed.

The authors of CCGM provide the following alternative definitions of a countable set:

Uncountable sets

There are a number of different definitions of an uncountable set, which all differ in the absence of countable choice:

  • SS is indenumerable if every function ff from N\mathbf{N} to SS is not a bijection.
  • SS is split indenumerably indexed if every function ff from N\mathbf{N} to SS is not a split surjection.
  • SS is indenumerably indexed if every function ff from N\mathbf{N} to SS is not a surjection.
  • SS is strongly indenumerably indexed if every function ff from N\mathbf{N} to SS is strongly non-surjective in the sense that there exists an element of SS that is not in the image of ff.
  • Suppose SS is an inequality space. Then SS is #\#-indenumerably indexed, or the pair (S,#)(S,\#) is strongly indenumerably indexed (or just indenumerable if context is clear) if every function ff from N\mathbf{N} to SS (or equivalently any variation as in the previous paragraph) 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.
  • SS is uncountable if every function ff from a detachable subset of N\mathbf{N} to SS is not a bijection.
  • SS is split uncountably indexed if every function ff from a detachable subset of N\mathbf{N} to SS is not a split surjection.
  • SS is uncountably indexed if every function ff from a detachable subset of N\mathbf{N} to SS is not a surjection.
  • SS is strongly uncountably indexed if every function ff from a detachable subset of N\mathbf{N} to SS is strongly non-surjective in the sense that there exists an element of SS that is not in the image of ff.
  • Suppose SS is an inequality space. Then SS is #\#-uncountably indexed, or the pair (S,#)(S,\#) is strongly uncountably indexed (or just uncountable if context is clear) if every function ff from a detachable subset of N\mathbf{N} to SS (or equivalently any variation as in the previous paragraph) 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.

Similarly as the case for above, the terms are even less standardised here. Certainly it is common for ‘uncountable’ to mean uncountably indexed, and yet it may also (as in classical mathematics) mean indenumerable.

We make the distinction between uncountable and uncountably indexed and between indenumerable and indenumerably indexed because in neutral constructive mathematics it is consistent that there exist a set which is both indenumerable and indenumerably indexed. However, similarly to countably indexed sets, in the presence of countable choice, the difference between uncountably indexed and split uncountably indexed and indenumerably indexed and split indenumerably indexed disappear.

There is a lot of freedom in defining uncountably indexed sets. You can start with countable 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!

Examples and Properties

In classical mathematics, the set of real numbers is uncountable. Even in constructive mathematics, the MacNeille real numbers, the Dedekind real numbers, and the Cauchy real numbers are all uncountable, in the sense of having a bijection with a countable set.

More generally, it is impossible for the real numbers to be both subcountable and countably indexed at the same time; subcountability implies that the real numbers have decidable equality because the natural numbers have decidable equality and injections preserve and reflect decidable equality, from which one can derive WLPO allowing one to prove that the real numbers are uncountably indexed by any of the usual arguments, resulting in a contradiction.

In fact, WLPO itself is sufficient to prove that the real numbers are uncountably indexed. However, it is consistent that, absent WLPO, the Dedekind real numbers are denumerably indexed and thus not uncountably indexed (cf Bauer 2022).

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 countably indexed xor uncountably indexed. Even constructively, a countably indexed set cannot be uncountably indexed. In Russian constructivism, however, there are subcountably indexed sets that are also uncountably indexed. In particular, the set of computable numbers is subcountably indexed, while the set of real numbers is uncountably indexed, 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.

History

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.

References

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

Some classically equivalent but constructively different definitions of a countable set can be found in

That in the absence of countable choice and excluded middle it is consistent that the Dedekind real numbers are denumerably indexed:

Last revised on November 17, 2024 at 02:15:41. See the history of this page for a list of all contributions to it.