A non-concise formula in the integer Heisenberg group

Abstract

A first-order formula in the language of groups is concise in a class of groups if, in every group in that class, finiteness of its solution set implies finiteness of the subgroup generated by that set. We give a parameter-free positive formula with one free variable that is not concise in the class of residually finite groups, answering Problem 21.106 of the Kourovka Notebook negatively. The counterexample is the integer Heisenberg group: the formula defines exactly the two generators of its infinite cyclic centre. More generally, over any commutative ring with identity, the same formula defines the central elements whose third coordinate is a unit. The proof uses a determinant identity and explicit witnesses for the quantifiers. Reduction of coordinates modulo positive integers establishes residual finiteness. The example is generated by two elements, torsion-free, and nilpotent of class two. The formula and the stated group-theoretic results have been formalized in Lean 4 using Mathlib.