Is there a finite theory of groups whose models are all torsion-free? We know from a standard ultrafilter argument (see this and this answer) that there cannot be a finite first-order theory that is modeled by precisely all the torsion-free groups.
But is there a finite theory $T$ that identifies only some torsion-free groups?
Furthermore, is there an example that has at least two models who are not elementarily equivalent?
 A: As mentioned in a comment, the theory of the trivial group works. However, let's assume that the given theory has a nontrivial model.
The answer is yes.
Indeed, by this answer by James Hyde to this question of mine, Thompson's group $F$ is definably left-orderable.
So there exists a formula $W(a,x,y)$, where $a$ means a $n$-tuple, $x$, $y$ are elements, such that for some $b\in F^n$, the relation $x\le y$ iff $W(b,x,y)$ defines a left-invariant total ordering on $F$.
One can therefore define a parameter-free formula $W'$ in the language of groups expressing that there exists $b$ such that $W(b,x,y)$ defines a left-invariant total ordering. So $W'$ is satisfied by $F$, and every group satisfying $W'$ is left-orderable, hence torsion-free.
(The uniqueness is not really relevant: one can define a formula for "being trivial or satifying $W'$.)

In contrast I think one can check that for abelian group, every formula that is satisfied by some nontrivial torsion-free abelian group $G$, is satisfied by at least one non-torsion-free abelian group (I think it's satisfied by $G\times\mathbf{Z}/p\mathbf{Z}$ for all large enough primes $p$).
