In mathematical logic, especially set theory and model theory, the back-and-forth method is a method for showing isomorphism between countably infinite structures satisfying specified conditions. In particular it can be used to prove that
any two countably infinite densely ordered sets (i.e., linearly ordered in such a way that between any two members there is another) without endpoints are isomorphic. An isomorphism between linear orders is simply a strictly increasing bijection. This result implies, for example, that there exists a strictly increasing bijection between the set of all rational numbers and the set of all real algebraic numbers.
any two countably infinite atomless Boolean algebras are isomorphic to each other.
any two equivalent countable atomic models of a theory are isomorphic.
the Erdős–Rényi model of random graphs, when applied to countably infinite graphs, almost surely produces a unique graph, the Rado graph.
any two many-complete recursively enumerable sets are recursively isomorphic.
As an example, the back-and-forth method can be used to prove Cantor's isomorphism theorem, although this was not Georg Cantor's original proof. This theorem states that two unbounded countable dense linear orders are isomorphic.
Suppose that
(A, ≤A) and (B, ≤B) are linearly ordered sets;
They are both unbounded, in other words neither A nor B has either a maximum or a minimum;
They are densely ordered, i.e. between any two members there is another;
They are countably infinite.
Fix enumerations (without repetition) of the underlying sets:
A = { a1, a2, a3, ... },
B = { b1, b2, b3, ... }.
Now we construct a one-to-one correspondence between A and B that is strictly increasing. Initially no member of A is paired with any member of B.
(1) Let i be the smallest index such that ai is not yet paired with any member of B. Let j be some index such that bj is not yet paired with any member of A and ai can be paired with bj consistently with the requirement that the pairing be strictly increasing. Pair ai with bj.