Cantor's isomorphism theorem

In order theory and model theory, branches of mathematics, Cantor's isomorphism theorem states that every two countable dense unbounded linear orders are 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 numbers and the numerical ordering of the dyadic rationals. The theorem is named after Georg Cantor, who first published it in 1895, using it to characterize the (uncountable) ordering on the real numbers. 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 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. 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 transitive law. The familiar numeric orderings on the integers, rational numbers, and real numbers are all examples of linear orders. 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.