A non-concise formula in the integer Heisenberg group

Problem

Is every parameter-free first-order group formula with one free variable concise in residually finite groups?

G_\varphi=\{g\in G:G\models\varphi(g)\},\qquad |G_\varphi|<\infty\quad\stackrel{?}{\Longrightarrow}\quad |\langle G_\varphi\rangle|<\infty.

This concerns formulas with quantifiers, not only group words. The counterexample uses a positive formula in a torsion-free nilpotent group of class two.

Setup and result

Let $\varphi(z)$ be a parameter-free first-order formula in the group language $\{1,\cdot,{}^{-1}\}$ . For a group $G$ , write

G_\varphi=\{g\in G:G\models\varphi(g)\}, \qquad \varphi(G)=\langle G_\varphi\rangle.

The formula $\varphi$ is concise in a class $\mathcal C$ of groups if $G_\varphi$ finite implies $\varphi(G)$ finite for every $G\in\mathcal C$ . Conte and Petschick (2) study this extension of conciseness from group words to first-order formulae. Problem 21.106 of the Kourovka Notebook (4) asks whether every formula with one free variable is concise in the class of residually finite groups.

Throughout, the commutator convention is $[g,h]=g^{-1}h^{-1}gh$ . Consider the formula

\tag{2} \begin{aligned} \Phi(z):={}&\exists a\,\exists b\,\forall x\,\forall y\,\exists r\,\exists s\\ &\bigl(z=[a,b]\ \land\ [r,a]=1\ \land\ [s,b]=1\\ &\qquad{}\land\ [r,b]=[x,y]\ \land\ [a,s]=[x,y]\bigr). \end{aligned}

Each commutator abbreviates a term in the group language. Thus $z$ is the only free variable, and no group elements occur as parameters. The formula is positive, since its quantifier-free part is a conjunction of equations.

Theorem 1. Let $H=\mathrm{H}(\mathbb{Z})$ be the integer Heisenberg group, with multiplication

(a,b,c)(d,e,f)=(a+d,b+e,c+f+ae).

Then

\begin{gathered} H_\Phi=\{(0,0,1),(0,0,-1)\},\\ \Phi(H)=Z(H)=\{(0,0,n):n\in\mathbb{Z}\}\cong(\mathbb{Z},+). \end{gathered}

Moreover, $H$ is residually finite, generated by two elements, torsion-free, and nilpotent of class exactly two. In particular, $\Phi$ is not concise in the class of residually finite groups.

Conte and Petschick prove that every existential formula is concise in torsion-free groups of nilpotency class two (2, Theorem 1.1). The universal quantifiers in (2) allow a counterexample in this same class. Further positive results for other classes of groups are obtained by Ciobanu and Conte (1). The question about group words in Problem 21.105 of (4) is distinct from the question answered here.

A formula defining units

Let $R$ be a commutative ring with identity. We realize the Heisenberg group $\mathrm{H}(R)$ as the set $R^3$ with the multiplication in Theorem 1. These coordinates correspond to the upper unitriangular matrices

(a,b,c)\longleftrightarrow \begin{pmatrix}1&a&c\\0&1&b\\0&0&1\end{pmatrix}.

The identity is $(0,0,0)$ , and

(a,b,c)^{-1}=(-a,-b,-c+ab).

For $t\in R$ , put $c_t=(0,0,t)$ . For $g=(g_1,g_2,g_3)$ and $h=(h_1,h_2,h_3)$ , write

\Delta(g,h)=g_1h_2-g_2h_1.

Direct multiplication gives

\tag{8} [g,h]=c_{\Delta(g,h)},\qquad c_tc_u=c_{t+u}.

Every $c_t$ is central. We use $R^\times$ for the group of units of $R$ , identifying a unit with its underlying ring element.

Proposition 2. For every commutative ring $R$ with identity,

\mathrm{H}(R)_\Phi=\{c_u:u\in R^\times\}.

Proof. Suppose that $\Phi(z)$ holds, and fix witnesses $a,b$ for the first two existential quantifiers. Apply the universal quantifiers to $x=(1,0,0)$ and $y=(0,1,0)$ . Since $[x,y]=c_1$ , the resulting witnesses $r,s$ satisfy

\begin{gather*} z=c_{\Delta(a,b)},\qquad \Delta(r,a)=\Delta(s,b)=0,\\ \Delta(r,b)=\Delta(a,s)=1. \end{gather*}

The determinant identity

\tag{11} \Delta(a,b)\Delta(r,s) =\Delta(r,a)\Delta(s,b)+\Delta(r,b)\Delta(a,s)

follows by expansion over $R$ . Substitution yields $\Delta(a,b)\Delta(r,s)=1$ , so $\Delta(a,b)$ is a unit.

Conversely, let $u\in R^\times$ , and choose $v\in R$ with $uv=1$ . Set $a=(1,0,0)$ and $b=(0,u,0)$ . For arbitrary $x,y\in\mathrm{H}(R)$ , put $t=\Delta(x,y)$ and take

r=(vt,0,0),\qquad s=(0,t,0).

Equation (8) gives

[a,b]=c_u,\qquad [r,a]=[s,b]=1,\qquad [r,b]=c_{vtu}=c_t=[a,s].

Since $[x,y]=c_t$ , all five equations in (2) hold with $z=c_u$ . The elements $a,b$ depend only on $u$ , whereas $r,s$ are chosen after $x,y$ , as required. ◻

The integer counterexample

Proof of Theorem 1. The units of $\mathbb{Z}$ are $1$ and $-1$ . Proposition 2 therefore gives $H_\Phi=\{c_1,c_{-1}\}$ . These two elements are distinct. By (8), $c_1^n=c_n$ for every $n\in\mathbb{Z}$ , so

\Phi(H)=\langle c_1,c_{-1}\rangle=\{c_n:n\in\mathbb{Z}\}.

The map $n\mapsto c_n$ is an injective homomorphism from $(\mathbb{Z},+)$ onto this subgroup. In particular, the subgroup is infinite.

Put $X=(1,0,0)$ and $Y=(0,1,0)$ . If $g=(a,b,c)$ is central, then (8) gives $[g,X]=c_{-b}=1$ and $[g,Y]=c_a=1$ . Thus $a=b=0$ , proving $Z(H)=\{c_n:n\in\mathbb{Z}\}$ .

We next verify residual finiteness. Recall that a group is residually finite if every nonidentity element has nonidentity image under some homomorphism to a finite group. For each positive integer $m$ , coordinate reduction defines a surjective homomorphism

\pi_m:H\longrightarrow\mathrm{H}(\mathbb{Z}/m\mathbb{Z}).

The homomorphism property follows from the multiplication formula, and the target has $m^3$ elements. If $g\ne1$ , choose a nonzero coordinate $t$ of $g$ and take $m=|t|+1$ . Then $0<|t|<m$ , so $m\nmid t$ and $\pi_m(g)\ne1$ .

Finally, $[X,Y]=c_1$ and, for every $(a,b,c)\in H$ ,

(a,b,c)=X^aY^b c_{c-ab}.

Hence $X,Y$ generate $H$ . All commutators are central by (8), and $[X,Y]\ne1$ , so $H$ has nilpotency class exactly two. The projection $(a,b,c)\mapsto(a,b)$ is a homomorphism to $(\mathbb{Z}^2,+)$ . If an element of $H$ has finite order, its first two coordinates therefore vanish. Such an element is $c_t$ , and $c_t^k=c_{kt}$ for every positive integer $k$ ; hence it has finite order only when $t=0$ . This proves torsion-freeness and completes the proof. ◻

References

Preprint · Lean (GitHub)

L. Ciobanu and M. Conte, Concise formulae in groups of non-positive curvature, preprint, 2026, arXiv:2605.06023.

M. Conte and J. M. Petschick, Conciseness of first-order formulae, Monatsh. Math. 209 (2026), 215–240. https://doi.org/10.1007/s00605-025-02127-5.

L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction—CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625–635. https://doi.org/10.1007/978-3-030-79876-5_37.

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st ed., 2026, Problem 21.106, p. 183, arXiv:1401.0300v46.

The mathlib Community, The Lean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, pp. 367–381. https://doi.org/10.1145/3372885.3373824.