# Are there any interesting theorems of first-order group theory

I've heard that theoremhood in first-order group theory is uncomputable, so there should be some theorems that are difficult to prove. However the few theorems of group theory I know are about subgroups, exponents and such, so they don't seem to be formalizable in first-order logic (for each $$n\in\mathbb{N}$$ we can write $$\forall_x x^n=e$$ for "the group has exponent $$n$$" but this doesn't seem to help much).

Are there any cool theorems or conjectures that are naturally stated in the first-order language of group theory?

• I agree that most of group theory is concerned with properties that are not first-order. First-order group theory is undecidable because the problem of determining whether a finitely presented group is trivial is undecidable (see the references in the Wikipedia link for details). You can express lots of theorems about specific group presentations in first-order group theory. E.g., the theorem that the group with generators $x\neq y$ with $x^3 = y^2 = (xy)^2 = 1$ has six elements. May 16, 2021 at 23:37
• @RobArthan how to state it in FOL? How does one prevent the existence of another generator (perhaps not the best phrasing)? May 18, 2021 at 4:53
• You might find math.mit.edu/~poonen/slides/rademacher2.pdf interesting. Also, en.wikipedia.org/wiki/Word_problem_for_groups#Examples and mathoverflow.net/questions/223624/… May 20, 2021 at 13:19
• @RobArthan Group theory is undecidable, but not because of the word problem. The undecidability of group theory preceded the unsolvability of the word problem by half a decade. The proof is due to Tarski: he gives a finitely axiomatized extension of group theory that he can show to be at least as difficult as Robinson's Q (already known to be undecidable at the time). May 20, 2021 at 15:18
• @Z.A.K. Agreed. That was not one of my best comments! May 20, 2021 at 16:16

It is proved in [1] that a finite group is soluble if and only if it satisfies the following first order sentence, which states that no non-trivial element $$g$$ is a product of $$56$$ commutators of pairs of conjugates of $$g$$: $$\forall g\ \forall x_1 \dotsm \forall x_{56}\ \forall y_1 \dotsm \forall y_{56}\ \bigl(g = 1 \vee g \not= [g^{x_1}, g^{y_1}] \dotsm [g^{x_{56}}, g^{y_{56}}]\bigr)$$

[1] J. S. Wilson – Finite axiomatization of finite soluble groups, J. London Math. Soc. (2) 74 (2006), 566–582.

There are actually many model-theoretic questions related to groups. You might be interested in the following questions (and even more by their answer) from this site

and from MathOverflow

Since you are looking for difficult theorems, let me mention the solution to Tarski's conjectures. Quoting Wikipedia,

Around 1945, Alfred Tarski asked whether the free groups on two or more generators have the same first-order theory, and whether this theory is decidable. Sela [2] answered the first question by showing that any two nonabelian free groups have the same first-order theory, and Kharlampovich & Myasnikov [1] answered both questions, showing that this theory is decidable.

A similar unsolved (as of 2011) question in free probability theory asks whether the von Neumann group algebras of any two non-abelian finitely generated free groups are isomorphic.

[1] O. Kharlampovich and A. Myasnikov, Elementary theory of free non-abelian groups, Journal of Algebra 302 no 2,‎ 2006, p. 451–552.

[2] Z. Sela, Diophantine geometry over groups. VI. The elementary theory of a free group, Geom. Funct. Anal. 16 (3), 2006, 707–730

This is a very active research topic. See for instance this recent paper:

[3] S. André, J. Fruchter, Formal solutions and the first-order theory of acylindrically hyperbolic groups

• This answer provides some interesting links about connections between logic and group theory but doesn't really answer the question. May 23, 2021 at 12:30