Model theory in group theory I am interested in useful results for group theorists that can be shown using model theory. For example :

Theorem: Let $\langle X \mid R \rangle$ be presentation of a group $G$ with $X$ finite and $R$ infinite. If $G$ is finitely presented then there exists $R' \subset R$ finite such that $\langle X \mid R' \rangle$ is a presentation of $G$.

A possible proof is to use compactness theorem or Gödel's completeness theorem. This result can be used to show that some groups are not finitely presented.
Do you know other such results?
 A: The space of marked groups can be used to show some properties of surface groups. For example, see the following question: Is the center of the fundamental group of the double torus trivial?
I found also some interesting results in the appendix of Model Theory by Hodges.
Consider the following problem: If $A,B,C$ are three groups such that $A \times C \simeq B \times C$; when $A$ and $B$ are isomorphic? For example:

Theorem: Let $G$ and $H$ be finitely generated finite-by-nilpotent groups. Then $G \times \mathbb{Z} \simeq H \times \mathbb{Z}$ iff $G$ and $H$ are elementary equivalent.

See Cancellation and Elementary Equivalence of Finitely Generated Finite-By-Nilpotent Groups or Cancellation of abelian groups of finite rank modulo elementary equivalence by Francis Oger.
Shelah solved the following problems using model theory:

Theorem: Any uncountable group $G$  of cardinality $\lambda$ has at least $\lambda$ subgroups not conjugate in pairs.  

See Uncountable groups have many nonconjugate subgroups.

Theorem: There is an uncountable group whose proper subgroups are all countable.

See On a problem of Kurosh, Johnson groups, and applications.
In On some conjectures connected with complete sentences, Makowski relates the problem "Is there an infinite finitely presented group with a finite number of conjugacy classes?" to the existence of a specific kind of theory (theorem 2.6).
A group $G$ is said linear of degree $n$ if it is embedable into $GL(n,F)$ for some field $F$. In Barwise's book, Handbook of mathematical logic, there is a proof of

Theorem: Let $G$ be a group. If every finitely-generated subgroup of $G$ is linear of degree $n$, then $G$ is linear of degree $n$.

A: Universal algebra can be viewed as model theory for a certain kind of nice theory, and in turn many basic facts about groups are theorems from universal algebra. e.g. the isomorphism theorems, the form of limits and equalizers and filtered colimits, the free and forgetful functors and their basic properties.
I'm not sure if this is the sort of thing you had in mind or not.
