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:

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:

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.

Suppose that

Fix enumerations (without repetition) of the underlying sets: