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.

We establish a language ${\displaystyle {\mathcal {L}}}$ and we consider two ${\displaystyle {\mathcal {L}}}$-structures ${\displaystyle {\mathcal {M}}}$ and ${\displaystyle {\mathcal {N}}}$ of domains respectively ${\displaystyle M}$ and ${\displaystyle N}$.

We call a partial isomorphism between ${\displaystyle {\mathcal {M}}}$ and ${\displaystyle {\mathcal {N}}}$ any isomorphism between two ${\displaystyle {\mathcal {L}}}$-substructures of ${\displaystyle {\mathcal {M}}}$ and ${\displaystyle {\mathcal {N}}}$.

A non-empty family ${\displaystyle {\mathcal {I}}}$ of partial isomorphisms between ${\displaystyle {\mathcal {M}}}$ and ${\displaystyle {\mathcal {N}}}$ is called a back-and-forth if both of the following properties hold:

• (FORTH) ${\displaystyle \forall \sigma \in {\mathcal {I}}\;\;\forall c\in M\;\;\exists \sigma '\in {\mathcal {I}}\;{\bigl (}\sigma \subseteq \sigma '\;\land \;c\in \mathrm {dom} (\sigma '){\bigr )}}$

• (BACK) ${\displaystyle \forall \sigma \in {\mathcal {I}}\;\;\forall d\in N\;\;\exists \sigma '\in {\mathcal {I}}\;{\bigl (}\sigma \subseteq \sigma '\;\land \;d\in \mathrm {im} (\sigma '){\bigr )}}$

In other words, each partial isomorphism of the family admits an extension which still belongs to the family itself. Moreover, one can find such an extension more precisely for each partial isomorphism, by imposing which new element must belong to the domain of the extension, or to its image (codomain).

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.^[1]

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 = { a₁, a₂, a₃, ... },

B = { b₁, b₂, b₃, ... }.

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 a_i is not yet paired with any member of B. Let j be some index such that b_j is not yet paired with any member of A and a_i can be paired with b_j consistently with the requirement that the pairing be strictly increasing. Pair a_i with b_j.

(2) Let j be the smallest index such that b_j is not yet paired with any member of A. Let i be some index such that a_i is not yet paired with any member of B and b_j can be paired with a_i consistently with the requirement that the pairing be strictly increasing. Pair b_j with a_i.

(3) Go back to step (1).

It still has to be checked that the choice required in step (1) and (2) can actually be made in accordance to the requirements. Using step (1) as an example:

If there are already a_p and a_q in A corresponding to b_p and b_q in B respectively such that a_p < a_i < a_q and b_p < b_q, we choose b_j in between b_p and b_q using density. Otherwise, we choose a suitable large or small element of B using the fact that B has neither a maximum nor a minimum. Choices made in step (2) are dually possible. Finally, the construction ends after countably many steps because A and B are countably infinite. Note that we had to use all the prerequisites.

According to Hodges (1993):

Back-and-forth methods are often ascribed to Cantor, Bertrand Russell and C. H. Langford [...], but there is no evidence to support any of these attributions.

While the theorem on countable densely ordered sets is due to Cantor (1895), the back-and-forth method with which it is now proved was developed by Edward Vermilye Huntington (1904) and Felix Hausdorff (1914). Later it was applied in other situations, most notably by Roland Fraïssé in model theory.

• Ehrenfeucht–Fraïssé game

• Hausdorff, F. (1914), Grundzüge der Mengenlehre
• Hodges, Wilfrid (1993), Model theory, Cambridge University Press, ISBN 978-0-521-30442-9
• Huntington, E. V. (1904), The continuum and other types of serial order, with an introduction to Cantor's transfinite numbers, Harvard University Press
• Marker, David (2002), Model Theory: An Introduction, Graduate Texts in Mathematics, Berlin, New York: Springer-Verlag, ISBN 978-0-387-98760-6