In recent years, surely the most important and influential (and, unfortunately, sometimes controversial) work on the first-order theory of groups has been Sela's work on free and hyperbolic groups, and also the parallel projects of Kharlampovich--Myasnikov.

In my opinion, the flow of ideas here is entirely in the opposite direction -- from group theory (and, in the case of Sela, geometry/topology) to logic. But one could perhaps say that the interest in logic has enabled the development of some tools that have proved useful for purely group-theoretic problems.

For instance, consider the study of the first-order theory of a non-abelian free group $F$. The very first thing one needs to understand is the set of solutions to a system of equations in a finite set of variables $x_1,\ldots,x_m$:

$~~~r_1(\underline{x})=1~,~\ldots~,~r_n(\underline{x})=1~$.

This solution set is tautologically the same thing as the set of homomorphisms $\mathrm{Hom}(G,F)$, where $G=\langle x_1,\ldots,x_m\mid r_1,\ldots,r_n\rangle$, and questions motivated by logic led to the development of a powerful set of tools for studying that set of homomorphisms.

As an example of a purely group-theoretic theorem that one can prove with these tools, I'll mention a theorem of Groves and myself.

**Theorem:** There is an algorithm that takes as input a finite presentation for a group $G$ and a solution to the word problem in $G$ and determines whether or not $G$ is free.

But, as I say, if you unpack the proof, it doesn't use any actual logic; only combinatorial, topological and geometric group theory.

4more comments