View source for Cantor's isomorphism theorem

{{good article}}
{{Short description|Uniqueness of countable dense linear orders}}
{{Use mdy dates|cs1-dates=ly|date=July 2021}}
{{Use list-defined references|date=July 2021}}
In [[order theory]] and [[model theory]], branches of mathematics, '''Cantor's isomorphism theorem''' states that every two countable [[dense order|dense]] unbounded [[Total order|linear orders]] are [[order isomorphism|order-isomorphic]]. For instance, [[Minkowski's question-mark function]] produces an isomorphism (a one-to-one order-preserving correspondence) between the numerical ordering of the [[rational number]]s and the numerical ordering of the [[dyadic rational]]s.

The theorem is named after [[Georg Cantor]], who first published it in 1895, using it to characterize the (uncountable) ordering on the [[real number]]s. It can be proved by a [[back-and-forth method]] that is also sometimes attributed to Cantor but was actually published later, by [[Felix Hausdorff]]. The same back-and-forth method also proves that countable dense unbounded orders are highly symmetric, and can be applied to other kinds of structures. However, Cantor's original proof only used the "going forth" half of this method. In terms of [[model theory]], the isomorphism theorem can be expressed by saying that the [[first-order theory]] of unbounded dense linear orders is [[Omega-categorical theory|countably categorical]], meaning that it has only one countable model, up to logical equivalence.

One application of Cantor's isomorphism theorem involves [[temporal logic]], a method for using logic to reason about time. In this application, the theorem implies that it is sufficient to use intervals of rational numbers to model intervals of time: using irrational numbers for this purpose will not lead to any increase in logical power.

==Statement and examples==
[[File:Minkowski question mark.svg|thumb|[[Minkowski's question-mark function]] provides a concrete isomorphism from rationals to dyadic rationals]]
Cantor's isomorphism theorem is stated using the following concepts:
*A [[linear order]] or total order is defined by a set of elements and a comparison operation that gives an ordering to each pair of distinct elements and obeys the {{nowrap|[[transitive relation|transitive law]].{{r|bmmn|dasgupta}}}} The familiar numeric orderings on the [[integer]]s, [[rational number]]s, and [[real number]]s are all examples of linear {{nowrap|orders.{{r|dasgupta}}}}
*Unboundedness means that the ordering does not contain a minimum or maximum element. This is different from the concept of a [[bounded set]] in a [[metric space]]. For instance, the [[open interval]] (0,1) is unbounded as an ordered set, even though it is bounded as a subset of the real numbers, because neither its [[infimum]] 0 nor its [[supremum]] 1 belong to the interval.{{r|bmmn}} The integers, rationals, and reals are also {{nowrap|unbounded.{{r|dasgupta}}}}
*An ordering is [[Dense order|dense]] when every pair of elements has another element between {{nowrap|them.{{r|bmmn}}}} This is different from being a topologically [[dense set]] within the real {{nowrap|numbers.{{r|dasgupta}}}} The rational numbers and real numbers are dense in this sense, as the [[arithmetic mean]] of any two numbers belongs to the same set and lies between them, but the integers are not dense because is no other integer between any two consecutive {{nowrap|integers.{{r|chalkdust}}}}
*The integers and rational numbers both form [[countable set]]s, but the real numbers do not, by a different result of Cantor, his [[Cantor's first uncountability proof|proof that the real numbers are uncountable]].{{r|dasgupta}}
*Two linear orders are [[order isomorphism|order-isomorphic]] when there exists a [[bijection|one-to-one correspondence]] between them that preserves their {{nowrap|ordering.{{r|bmmn|dasgupta}}}} For instance, the integers and the [[even number]]s are order-isomorphic, under a bijection that multiplies each integer {{nowrap|by two.{{r|chalkdust}}}}
With these definitions in hand, Cantor's isomorphism theorem states that every two unbounded countable dense linear orders are {{nowrap|order-isomorphic.{{r|bmmn}}}}

Within the rational numbers, certain subsets are also countable, unbounded, and dense. The rational numbers in the open unit interval are an example. Another example is the set of [[dyadic rational]] numbers, the numbers that can be expressed as a fraction with an integer numerator and a [[power of two]] as the denominator. By Cantor's isomorphism theorem, the dyadic rational numbers are order-isomorphic to the whole set of rational numbers. In this example, an explicit order isomorphism is provided by [[Minkowski's question-mark function]].{{r|girgensohn}} Another example of a countable unbounded dense linear order is given by the set of real [[algebraic number]]s, the real roots of polynomials with integer coefficients. In this case, they are a superset of the rational numbers, but are again {{nowrap|order-isomorphic.{{r|bosmet}}}} It is also possible to apply the theorem to other linear orders whose elements are not defined as numbers. For instance, the binary [[string (computer science)|strings]] that end in a 1, in their [[lexicographic order]], form another isomorphic {{nowrap|ordering.{{r|lohmat}}}}

==Proofs==
One proof of Cantor's isomorphism theorem, in some sources called "the standard {{nowrap|proof",{{r|bryant}}}} uses the [[back-and-forth method]]. This proof builds up an isomorphism between any two given orders, using a [[greedy algorithm]], in an ordering given by a countable enumeration of the two orderings. In more detail, the proof maintains two order-isomorphic finite subsets <math>A</math> and <math>B</math> of the two given orders, initially empty. It repeatedly increases the sizes of <math>A</math> and <math>B</math> by adding a new element from one order, the first missing element in its enumeration, and matching it with an order-equivalent element of the other order, proven to exist using the density and lack of endpoints of the order. The two orderings switch roles at each step: the proof finds the first missing element of the first order, adds it to <math>A</math>, matches it with an element of the second order, and adds it to <math>B</math>; then it finds the first missing element of the second order, adds it to <math>B</math>, matches it with an element of the first order, and adds it to <math>A</math>, etc. Every element of each ordering is eventually matched with an order-equivalent element of the other ordering, so the two orderings are {{nowrap|isomorphic.{{r|silver}}}}

Although the back-and-forth method has also been attributed to Cantor, Cantor's original publication of this theorem in 1895–1897 used a different {{nowrap|proof.{{r|silver}}}} In an investigation of the history of this theorem by logician Charles L. Silver, the earliest instance of the back-and-forth proof found by Silver was in a 1914 textbook by {{nowrap|[[Felix Hausdorff]], his ''[[Grundzüge der Mengenlehre]]''.{{r|silver}}}}

Instead of building up order-isomorphic subsets <math>A</math> and <math>B</math> by going "back and forth" between the enumeration for the first order and the enumeration for the second order, Cantor's original proof only uses the "going forth" half of the back-and-forth {{nowrap|method.{{r|bmmn}}}} It repeatedly augments the two finite sets <math>A</math> and <math>B</math> by adding to <math>A</math> the first missing element of the first order's enumeration, and adding to <math>B</math> the order-equivalent element that is first in the second order's enumeration. This naturally finds an equivalence between the first ordering and a subset of the second ordering, and Cantor then argues that the entire second ordering is {{nowrap|included.{{r|bmmn|silver}}}}

The back-and-forth proof has been formalized as a [[Automated theorem proving|computer-verified proof]] using [[Coq (software)|Coq]], an [[interactive theorem prover]]. This formalization process led to a strengthened result that when two [[Computably enumerable set|computably enumerable]] linear orders have a computable comparison predicate, and computable functions representing their density and unboundedness properties, then the isomorphism between them is also {{nowrap|computable.{{r|kirst}}}}

==Model theory==
One way of describing Cantor's isomorphism theorem uses the language of [[model theory]]. The [[first-order theory]] of unbounded dense linear orders consists of sentences in mathematical logic concerning variables that represent the elements of an order, with a [[binary relation]] used as the comparison operation of the ordering. Here, a sentence means a [[well-formed formula]] that has no [[free variable]]s. These sentences include both axioms, formulating in logical terms the requirements of a dense linear order, and all other sentences that can be proven as logical consequences from those axioms. The axioms of this system can be expressed {{nowrap|as:{{r|goldrei|worrell}}}}
{| class=wikitable
|+ 
! Axiom
! Explanation
|-
| <math>\forall a\,\bigl(\lnot(a < a)\bigr)</math>
| Comparison is [[Reflexive relation|irreflexive]]: no element is less than itself.
|-
| <math>\forall a\,\forall b\,(a= b\vee a< b\vee b< a)</math>
| Comparison is [[Connected relation|connected]] or total, meaning every two distinct elements are comparable.
|-
| <math>\forall a\,\forall b\,\forall c\,\bigl((a< b\wedge b< c)\Rightarrow a< c\bigr)</math>
| Comparison is [[Transitive relation|transitive]]: each triple of elements is consistently ordered.
|-
| <math>\forall a\,\exists b\,(b<a)</math>
| There is no lower bound; every element <math>a</math> has a smaller element <math>b</math>.
|-
| <math>\forall a\,\exists b\,(a<b)</math>
| There is no upper bound; every element <math>a</math> has a larger element <math>b</math>.
|-
| <math>\forall a\,\forall b\,\bigl(a<b\Rightarrow\exists c\,(a<c\wedge c<b)\bigr)</math>
| The order is dense: every two elements <math>a</math> and <math>b</math> have an element <math>c</math> between them.
|}

A model of this theory is any system of elements and a comparison relation that obeys all of the axioms; it is a ''countable model'' when the system of elements forms a [[countable set]]. For instance, the usual comparison relation on the rational numbers is a countable model of this theory. Cantor's isomorphism theorem can be expressed by saying that the first-order theory of unbounded dense linear orders is [[Omega-categorical theory|countably categorical]]: it has only one countable model, up to logical {{nowrap|equivalence.{{r|bmmn|bd}}}} However, it is not [[Categorical theory|categorical for higher cardinalities]]: for any higher [[cardinality]], there are multiple inequivalent dense unbounded linear orders with the same {{nowrap|cardinality.{{r|morley}}}}

A method of [[quantifier elimination]] in the first-order theory of unbounded dense linear orders can be used to prove that it is a [[complete theory]]. This means that every logical sentence in the language of this theory is either a theorem, that is, provable as a logical consequence of the axioms, or the negation of a theorem. This is closely related to being categorical (a sentence is a theorem if it is true of the unique countable model; see the [[Łoś–Vaught test]]) but there can exist multiple distinct models that have the same complete theory. In particular, both the ordering on the rational numbers and the ordering on the real numbers are models of the same theory, even though they are different models. Quantifier elimination can also be used in an [[algorithm]] for deciding whether a given sentence is a {{nowrap|theorem.{{r|worrell}}}}

==Related results==
[[File:Monotone piecewise linear.svg|thumb|The graph of a piecewise linear order automorphism of rational numbers taking the four points {1,4,5,8} to {3,4,6,7}]]
The same back-and-forth method used to prove Cantor's isomorphism theorem also proves that countable dense linear orders are highly symmetric. Their symmetries are called [[order automorphism]]s, and consist of order-preserving bijections from the whole linear order to itself. By the back-and-forth method, every countable dense linear order has order automorphisms that map any set of <math>k</math> points to any other set of <math>k</math> points. This can also be proven directly for the ordering on the rationals, by constructing a [[piecewise linear function|piecewise linear]] order automorphism with breakpoints at the <math>k</math> given points. This equivalence of all {{nowrap|<math>k</math>-element}} sets of points is summarized by saying that the group of symmetries of a countable dense linear order is "highly homogeneous". However, there is no order automorphism that maps an [[ordered pair]] of points to its reverse, so these symmetries do not form a {{nowrap|[[2-transitive group]].{{r|bmmn}}}}

The isomorphism theorem can be extended to colorings of an unbounded dense countable linear ordering, with a finite or countable set of colors, such that each color is dense, in the sense that a point of that color exists between any other two points of the whole ordering. The subsets of points with each color partition the order into a family of unbounded dense countable linear orderings. Any partition of an unbounded dense countable linear orderings into subsets, with the property that each subset is unbounded (within the whole set, not just in itself) and dense (again, within the whole set) comes from a coloring in this way. Each two colorings with the same number of colors are order-isomorphic, under any permutation of their colors. {{harvtxt|Bhattacharjee|Macpherson|Möller|Neumann|1997}} give as an example the partition of the rational numbers into the [[dyadic rational]]s and their complement; these two sets are dense in each other, and their union has an order isomorphism to any other pair of unbounded linear orders that are countable and dense in each other. Unlike Cantor's isomorphism theorem, the proof needs the full back-and-forth argument, and not just the "going forth" {{nowrap|argument.{{r|bmmn}}}}

Cantor used the isomorphism theorem to characterize the ordering of the [[real number]]s, an uncountable set. Unlike the rational numbers, the real numbers are [[Dedekind-complete]], meaning that every subset of the reals that has a finite upper bound has a real least upper bound. They contain the rational numbers, which are dense in the real numbers. By applying the isomorphism theorem, Cantor proved that whenever a linear ordering has the same properties of being Dedekind-complete and containing a countable dense unbounded subset, it must be order-isomorphic to the real {{nowrap|numbers.{{r|jech}}}} [[Suslin's problem]] asks whether orders having certain other properties of the order on the real numbers, including unboundedness, density, and completeness, must be order-isomorphic to the reals; the truth of this statement is independent of [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]] {{nowrap|(ZFC).{{r|dj}}}}

Although uncountable unbounded dense orderings may not be order-isomorphic, it follows from the back-and-forth method that any two such orderings are [[elementarily equivalent]].{{r|bryant|langford}} Another consequence of Cantor's proof is that every finite or countable linear order can be embedded into the rationals, or into any unbounded dense ordering. Calling this a "well known" result of Cantor, [[Wacław Sierpiński]] proved an analogous result for higher cardinality: assuming the [[continuum hypothesis]], there exists a linear ordering of cardinality <math>\aleph_1</math> into which all other linear orderings of cardinality <math>\aleph_1</math> can be {{nowrap|embedded.{{r|sierpinski}}}} [[Baumgartner's axiom]], formulated by [[James Earl Baumgartner]] in 1973 to study the continuum hypothesis, concerns {{nowrap|<math>\aleph_1</math>-dense}} sets of real numbers, unbounded sets with the property that every two elements are separated by exactly <math>\aleph_1</math> other elements. It states that each two such sets are order-isomorphic, providing in this way another higher-cardinality analogue of Cantor's isomorphism theorem (<math>\aleph_1</math> is defined as the cardinality of the set of all countable ordinals). Baumgartner's axiom is consistent with ZFC and the negation of the continuum hypothesis, and implied by the {{nowrap|[[proper forcing axiom]],{{r|baumgartner}}}} but independent of {{nowrap|[[Martin's axiom]].{{r|as}}}}

In [[temporal logic]], various formalizations of the concept of an interval of time can be shown to be equivalent to defining an interval by a pair of distinct elements of a dense unbounded linear order. This connection implies that these theories are also countably categorical, and can be uniquely modeled by intervals of rational {{nowrap|numbers.{{r|vanben|ladkin}}}}

[[Sierpiński's theorem on metric spaces|Sierpiński's theorem]] stating that any two countable metric spaces without isolated points are homeomorphic can be seen as a topological analogue of Cantor's isomorphism theorem, and can be proved using a similar back-and-forth argument.

== References ==
{{reflist|refs=

<ref name=as>{{citation
 | last1 = Avraham | first1 = Uri
 | last2 = Shelah | first2 = Saharon | author2-link = Saharon Shelah
 | doi = 10.1007/BF02761858 | doi-access = 
 | issue = 1–2
 | journal = [[Israel Journal of Mathematics]]
 | mr = 599485
 | pages = 161–176
 | title = Martin's axiom does not imply that every two {{nowrap|<math>\aleph_{1}</math>-dense}} sets of reals are isomorphic
 | volume = 38
 | year = 1981}}</ref>

<ref name=baumgartner>{{citation
 | last = Baumgartner | first = James E. | author-link = James Earl Baumgartner
 | doi = 10.4064/fm-79-2-101-106
 | issue = 2
 | journal = [[Fundamenta Mathematicae]]
 | mr = 317934
 | pages = 101–106
 | title = All {{nowrap|<math>\aleph_{1}</math>-dense}} sets of reals can be isomorphic
 | volume = 79
 | year = 1973| doi-access = free
 }}</ref>

<ref name=bd>{{citation
 | last1 = Büchi | first1 = J. Richard | author-link = Julius Richard Büchi
 | last2 = Danhof | first2 = Kenneth J.
 | doi = 10.1002/malq.19730192604
 | journal = Zeitschrift für Mathematische Logik und Grundlagen der Mathematik
 | mr = 337567
 | pages = 411–426
 | title = Variations on a theme of Cantor in the theory of relational structures
 | volume = 19
 | year = 1973| issue = 26–29 }}</ref>

<ref name=bmmn>{{citation
 | last1 = Bhattacharjee | first1 = Meenaxi
 | last2 = Macpherson | first2 = Dugald
 | last3 = Möller | first3 = Rögnvaldur G.
 | last4 = Neumann | first4 = Peter M. | author4-link = Peter M. Neumann
 | contribution = Rational numbers
 | doi = 10.1007/978-93-80250-91-5_9
 | isbn = 81-85931-13-5
 | mr = 1632579
 | pages = 77–86
 | publisher = Springer-Verlag | location = Berlin
 | series = Texts and Readings in Mathematics
 | title = Notes on infinite permutation groups
 | volume = 12
 | year = 1997}}</ref>

<ref name=bosmet>{{citation
 | last1 = Bosi | first1 = G.
 | last2 = Mehta | first2 = G. B.
 | doi = 10.1016/S0304-4068(02)00058-7
 | issue = 3
 | journal = [[Journal of Mathematical Economics]]
 | mr = 1940365
 | pages = 311–328
 | title = Existence of a semicontinuous or continuous utility function: a unified approach and an elementary proof
 | volume = 38
 | year = 2002}}; see Remark 3, p. 323</ref>

<ref name=bryant>{{citation|title=A computation of partial isomorphism rank on ordinal structures|type=Doctoral dissertation|last=Bryant|first=Ross|publisher=University of North Texas|year=2006|id=305292986|page=1}}</ref>

<ref name=chalkdust>{{citation|title=Curiosities of linearly ordered sets|magazine=[[Chalkdust (magazine)|Chalkdust]]|first=Andrei|last=Chekmasov|date=October 23, 2019|url=https://chalkdustmagazine.com/features/curiosities-of-linearly-ordered-sets/}}</ref>

<ref name=dasgupta>{{citation
 | last = Dasgupta | first = Abhijit
 | contribution = Chapters 7 & 8: Orders and order types; Dense and complete orders
 | doi = 10.1007/978-1-4614-8854-5
 | pages = 131–174
 | publisher = Springer New York
 | title = Set Theory
 | year = 2014| doi-access = free
 | isbn = 978-1-4614-8853-8
 }}</ref>

<ref name=dj>{{citation
 | last1 = Devlin | first1 = Keith J. | author1-link = Keith Devlin
 | last2 = Johnsbråten | first2 = Håvard
 | mr = 0384542
 | publisher = Springer-Verlag | location = Berlin & New York
 | series = Lecture Notes in Mathematics | volume = 405
 | title = The Souslin problem
 | year = 1974}}</ref>

<ref name=girgensohn>{{citation
 | last = Girgensohn | first = Roland
 | doi = 10.1006/jmaa.1996.0370
 | issue = 1
 | journal = [[Journal of Mathematical Analysis and Applications]]
 | mr = 1412484
 | pages = 127–141
 | title = Constructing singular functions via Farey fractions
 | volume = 203
 | year = 1996| doi-access = free
 }}</ref>

<ref name=goldrei>For this axiomatization of strict linear orders, see: {{citation|title=Propositional and Predicate Calculus: A Model of Argument|first=Derek|last=Goldrei|publisher=Springer|year=2005|isbn=9781846282294|page=[https://books.google.com/books?id=edqwSVJ9GGQC&pg=PA193 193]}}. The axioms can be formulated logically using either a strict comparison <math><</math> or a non-strict comparison <math>\le</math> but the strict comparison simplifies the expression of the axioms for the properties of being unbounded and dense. Note that it is not necessary to specify that these orders are antisymmetric, that is, that <math>a<b\Rightarrow\lnot(b<a)</math>; this is a consequence of irreflexivity and transitivity.</ref>

<ref name=jech>{{citation
 | last = Jech | first = Thomas | author-link = Thomas Jech
 | at = Theorem 4.3, p. 38
 | doi = 10.1007/3-540-44761-X
 | edition = 3rd millennium
 | isbn = 3-540-44085-2
 | mr = 1940513
 | publisher = Springer-Verlag | location = Berlin
 | series = Springer Monographs in Mathematics
 | title = Set theory
 | year = 2003}}</ref>

<ref name=kirst>{{citation
 | last = Kirst | first = Dominik
 | editor1-last = Andronick | editor1-first = June
 | editor2-last = de Moura | editor2-first = Leonardo
 | contribution = Computational back-and-forth arguments in constructive type theory
 | doi = 10.4230/LIPIcs.ITP.2022.22
 | pages = 22:1–22:12
 | publisher = Schloss Dagstuhl – Leibniz-Zentrum für Informatik
 | series = LIPIcs
 | title = 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7–10, 2022, Haifa, Israel
 | volume = 237
 | year = 2022| doi-access = free
 }}</ref>

<ref name=ladkin>{{citation
 | last = Ladkin | first = Peter B.
 | editor1-last = Forbus | editor1-first = Kenneth D.
 | editor2-last = Shrobe | editor2-first = Howard E.
 | contribution = Models of axioms for time intervals
 | contribution-url = https://www.aaai.org/Library/AAAI/1987/aaai87-042.php
 | pages = 234–239
 | publisher = Morgan Kaufmann
 | title = Proceedings of the 6th National Conference on Artificial Intelligence. Seattle, WA, USA, July 1987
 | year = 1987}}</ref>

<ref name=langford>{{citation
 | last = Langford | first = C. H.
 | doi = 10.2307/1968352
 | issue = 1–4
 | journal = Annals of Mathematics
 | mr = 1502760
 | pages = 16–40
 | series = Second Series
 | title = Some theorems on deducibility
 | volume = 28
 | year = 1926–1927| jstor = 1968352
 }}</ref>

<ref name=lohmat>{{citation
 | last1 = Lohrey | first1 = Markus
 | last2 = Mathissen | first2 = Christian
 | doi = 10.1016/j.ic.2013.01.002
 | journal = Information and Computation
 | mr = 3016459
 | pages = 71–105
 | title = Isomorphism of regular trees and words
 | volume = 224
 | year = 2013| doi-access = free
 | arxiv = 1102.2782
 }}</ref>

<ref name=morley>{{citation
 | last = Morley | first = Michael
 | doi = 10.2307/1994188
 | journal = [[Transactions of the American Mathematical Society]]
 | mr = 175782
 | pages = 514–538
 | title = Categoricity in power
 | volume = 114
 | year = 1965| issue = 2
 | doi-access = free
 | jstor = 1994188
 }}</ref>

<ref name=sierpinski>{{citation
 | last = Sierpiński | first = Wacław | author-link = Wacław Sierpiński
 | doi = 10.4064/fm-18-1-280-284
 | journal = [[Fundamenta Mathematicae]]
 | language = fr
 | pages = 280–284
 | title = Généralisation d'un théorème de Cantor concernant les ensembles ordonnés dénombrables
 | volume = 18
 | year = 1932
 | zbl = 0004.20502| doi-access = free
 }}</ref>

<ref name=silver>{{citation
 | last = Silver | first = Charles L.
 | issue = 1
 | journal = Modern Logic
 | mr = 1253680
 | pages = 74–78
 | title = Who invented Cantor's back-and-forth argument?
 | url = https://projecteuclid.org/euclid.rml/1204835164
 | volume = 4
 | year = 1994}}</ref>

<ref name=vanben>{{citation
 | last = van Benthem | first = Johan
 | doi = 10.1305/ndjfl/1093870515
 | issue = 1
 | journal = Notre Dame Journal of Formal Logic
 | mr = 723616
 | pages = 1–16
 | title = Tense logic and time
 | volume = 25
 | year = 1984| doi-access = free
 }}</ref>

<ref name=worrell>{{citation|first=James|last=Worrell|title=Decidable theories|work=Logic and Proof|type=Lecture notes|publisher=University of Oxford|year=2016|url=http://www.cs.ox.ac.uk/james.worrell/lecture15-2015.pdf}}; Worrell uses a different but equivalent axiomatization for strict linear orders, and combines the two unboundedness axioms into a single axiom.</ref>

}}

{{Order theory|state=collapsed}}

[[Category:Model theory]]
[[Category:Order theory]]
[[Category:Georg Cantor]]
[[Category:Theorems in the foundations of mathematics]]