There seems to be an ever-growing literature on the first-order theory of groups. While I find this interaction between group theory and logic quite appealing, I was wondering the following:

Are there examples of applications of first-order logic to problems that are group-theoretic in nature (and do not involve the first-order theory of groups)?

To give an example of what I mean by that, an example from another field is (a proof of) the Ax-Grothendieck theorem, where ideas from model theory can be used to show a statement about the bijectivity of some polynomials. After a quick search on the internet, I couldn't find any such an application.

  • 4
    $\begingroup$ You can use the compactness of first orfer logic and completeness of the theory of the theory of an algebraically closed field of a fixed characteristic to prove finitely generated linear groups are residually finite. I am sure I wrote the proof in the answer to some questions. $\endgroup$ – Benjamin Steinberg Feb 10 '17 at 14:15
  • $\begingroup$ In my opinion a theorem about linear groups is not just group theory, since it involves a field. $\endgroup$ – YCor Feb 10 '17 at 15:58
  • 1
    $\begingroup$ May be of interest: math.stackexchange.com/questions/282144/… $\endgroup$ – Seirios Feb 10 '17 at 17:47
  • 1
    $\begingroup$ I can't find the mo question I wanted to link to. The point is you need commutative domains which are finitely generated over a field are residually finite. ThIs can be proved by compactness of logic and completeness properties of the theory of an algebraically closed field of fixed characteristic. $\endgroup$ – Benjamin Steinberg Feb 10 '17 at 18:26
  • 1
    $\begingroup$ I didn't claim it was the only way. Just like Ax-Grothendieck can use algebra or logic. $\endgroup$ – Benjamin Steinberg Feb 10 '17 at 20:16

One group theory topic in which logicians have been active is the automorphism tower problem.

The automorphism tower of a group $G$ is obtained by computing the automorphism group $\newcommand\Aut{\text{Aut}}\Aut(G)$, and then the automorphism group of that group $\Aut(\Aut(G))$ and so on. Each group maps into the next by inner automorphisms, and so one may continue the iteration transfinitely with the direct limit. The main question had been whether this process ever stops, and if so, how long it takes.

Simon Thomas, using an application of Fodor's lemma in set theory, showed that every centerless group $G$ has an automorphism tower that terminates before $(2^{|G|})^+$ steps. He had been writing a book on the topic, which was excellent, although I'm not sure if this is yet fully realized.

Greg Kuperberg wrote a nice summary answer to this classic MathOverflow question, Does $\Aut(\Aut(\cdots\Aut(G))))$ stabilize?.

My 1998 paper Every group has a terminating automorphism tower shows that every group has a terminating tower, and one can find other papers and talks (with slides) about the automorphism tower problem on my blog: jdh.hamkins.org/tag/automorphism-towers.

Perhaps one of the most interesting connection with logic is my joint result with Simon Thomas in our 2000 paper Changing the heights of automorphism towers, where we show that the very same group can have automorphism towers of vastly different heights, depending on the set-theoretic background universe in which the tower is computed.


One area where logic really helped group theory is the theory of zetafunctions of torsionfree nilpotent groups. Define $\zeta_G(s)=\sum_{U\leq G} (G:U)^{-s}$, where summation runs over all finite index subgroups. If $G$ is nilpotent, then this function decomposes as a product over subgroups of prime power index $\zeta_p$. Grunewald, Segal and Smith showed that $\zeta_p$ is a rational function in $p^{-s}$ by showing that $\zeta_p$ can be expressed in terms of a $p$-adic integral over a definable set of $p$-adic integers. Now Denef and Macintyre showed that the integral of a definable function over a definable set determines a rational function, and you get rationality of the local factors. The technique has further been developed and lead to motivic integration, which is useful not only for groups but also in algebraic gemotry.


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$:


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.

  • $\begingroup$ Could you clarify what you mean by taking a solution to the word problem in $G$ as input to another algorithm? Do you mean that your algorithm is computing from an oracle for the word problem of $G$? $\endgroup$ – Joel David Hamkins Feb 11 '17 at 23:13
  • $\begingroup$ @JoelDavidHamkins: One way to say it is that freeness is decidable in any set of presentations in which the word problem is uniformly decidable. $\endgroup$ – HJRW Feb 12 '17 at 7:11
  • $\begingroup$ Ah, that is much clearer. $\endgroup$ – Joel David Hamkins Feb 12 '17 at 12:14
  • $\begingroup$ But is my way of saying it also true? That would be a stronger result, since the uniform solution you mention would of course enable you to compute the oracle I mention, and also it would apply to more groups. $\endgroup$ – Joel David Hamkins Feb 12 '17 at 15:12
  • $\begingroup$ @JoelDavidHamkins: We have an algorithm that's uniform in the presentation for $G$, but needs to call a subroutine (oracle?) which can solve the word problem in $G$. I think that's the same as your way of saying it. I don't really see in practice how that applies to more groups, though. $\endgroup$ – HJRW Feb 12 '17 at 18:56

Even though the question in the body is specifically restricted to first-order logic, the question in the title is not, so I will give an example that uses the infinitary logic $\mathcal{L}_{\omega_1 \omega}$.

Recall that a group $G$ is said to be universal locally finite if it is locally finite, every finite group is embedded in $G$, and any two isomorphic finite subgroups of $G$ are isomorphic via an inner automorphism. Philip Hall showed that such groups do exist and that any two countable universal locally finite groups are isomorphic.

Kegel and Wehrfritz asked whether any two universal locally finite groups of cardinality $\kappa > \aleph_0$ are isomorphic. Shelah and Macintyre proved in this paper that the answer is negative. Their proof uses model-theoretic techniques in $\mathcal{L}_{\omega_1 \omega}$ to obtain models of every uncountable cardinality having countably many types over each countable subset.


L. van den Dries and A. J. Wilkie. Gromov’s theorem on groups of polynomial growth and elementary logic. J. Algebra, 89(2):349–374, 1984.


The application I had in mind was to proving Malcev's theorem that finitely generated linear groups are residually finite. If $G$ is generated by a finite symmetric generating subset $S$ and is linear over a field $K$ (which we may assume without loss of generality is algebraically closed), then $G$ embeds in some $GL_n(K)$. The matrix entries of the finite set $S$ generate a finitely generated integral domain $D$ over the prime ring $R$ of $K$. So $G$ is a finitely generated subgroup of $GL_n(D)$. If $D$ is residually finite as a ring, then $GL_n(D)$ is obviously residually finite as a group and hence $G$ is residually finite.

Since $D$ is a finitely generated domain over the prime ring $R$, by say some finite set $X$, and $R[X]$ is Noetherian, we deduce that $D=R[X]/I$ where $I$ is generated by some finite set $Z$ of polynomials. Suppose that $|X|=k$.

Then if $f\in R[X]$ with $f+I\neq I$, then the algebraically closed field $K$ satisfies the first order formula $\varphi$ in the language of rings asserting that there exist $x_1,\ldots, x_k$ such that $p(x_1,\ldots, x_k)=0$ for each $p\in Z$ and $f(x_1,\ldots, x_k)\neq 0$ (where we are slightly abusing notation since $R$ is either $\mathbb Z$ or $\mathbb Z/p$ for a prime $p$). If $R$ has characteristic $p>0$, i.e. $R=\mathbb Z/p$, then by the completeness of the theory of an algebraically closed field of characteristic $p$, it follows that $\varphi$ is true over the algebraic closure $\overline R$ of $R$, which means that $R[X]/I$ has a homomorphism into $\overline R$ sending $f+I$ to a non-zero element. Since the image of $R[X]/I$ is a finitely generated extension of $R=\mathbb Z/p$, it is finite. We conclude in this case that $D$ is residually finite.

If $R$ has characteristic $0$, i.e. $R=\mathbb Z$, then by a standard application of the compactness of first order logic (this can be found in Marker's text book) there is an algebraically closed field of positive characteristic $p>0$ for which the formula $\varphi$ is true. Now proceeding as in the previous case, we deduce that $f$ is non-zero in a finite image of $D$.


Here is a silly application that can be made less silly by generalizing from groups to semigroups.

Suppose you want to decide if a finite group $G$ has a faithful linear representation of degree $k$ over the complex numbers. The natural way to do this is to use known algorithms (going back to Burnside, but improved on by Dixon and Schneider) to compute the character table and then from there you can just check if there is a faithful character of degree $k$ by standard character theory.

Alternatively, one can observe that asking if a finite group $G$ has a faithful linear representation of degree $k$ is a first order statement in the language of rings over the complex numbers (in fact, it belongs to the existential theory since you are asking if there exist $|G|$ distinct $k\times k$ matrices that satisfy some polynomial equations in their entries). So by Tarski's theorem that the first order theory of the complex numbers is decidable you can decide this. In fact, the existential theory of the complex numbers is now known to be in PSPACE (and in fact if one assumes the generalized Riemann hypothesis it is known to be in a class not too far above NP, which is a lower bound on the existential theory). I have no idea how much better, if at all, is the complexity of the first algorithm I suggested.

Also, this observation, plus a compactness argument like in my other answer, shows that if $G$ has a faithful degree $k$ representation over the complex numbers, then it has a faithful degree $k$ representation over some finite field. Again, this can also be shown by direct algebraic arguments from algebra, but I like the logic proof.

One advantage of the logic approach to existence of a faithful degree $k$ linear representation over the complex numbers is that it applies verbatim to finite semigroups while I don't see how to adapt anything like the first approach to finite semigroups,


See the followings:

Malcev, A. I. On a general method for obtaining local theorems in group theory, Notices of the Pedagogical Institute of Ivanovo, Physical-Mathematical Sciences, 1, 3-9 (in Russian), 1941.




Let me to copy and paste the publisher summery of the latter link that I think it should be a the same as the first one:

Publisher Summary

In algebra, and especially in group theory, there are quite a few theorems of the form: if a certain property C holds for all subalgebras of a given algebra (group, ring, and others) generated by a finite set of elements of this algebra, then C holds for the whole algebra. It is shown that such propositions are not specifically algebraic in the majority of cases and can be obtained as immediate consequences of a general proposition of mathematical logic. This general approach to local theorems does not give the solutions to any difficult algebraic problems. In many cases, however, it makes the algebraic proofs of these theorems redundant, and sometimes permits one to see immediately that a theorem holds under somewhat broader assumptions. Thus, the propositions are introduced on solvable groups and groups with Sylow sequences only for the case of locally finite groups; the extension lattice isomorphisms is established for countable groups, and to give a proof valid for uncountable groups.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.