Elementary-Theory Classification of Virtually Free Groups

Definitions and mathematical statement

Let $L_{\mathrm{grp}}=\{1,\cdot,{}^{-1}\}$ be the first-order language of groups. A group is virtually free if it contains a free subgroup of finite index, and virtually cyclic if it contains a cyclic subgroup of finite index. The stated ambient class consists of finitely generated virtually free groups.

For groups $G,H$, write $G\equiv H$ if, for every $L_{\mathrm{grp}}$-sentence $\sigma$, \[ G\models\sigma\quad\Longleftrightarrow\quad H\models\sigma. \] For an injective homomorphism $\iota:G\to H$, say that $\iota$ is elementary if, for every integer $n\geq 0$, every $L_{\mathrm{grp}}$-formula $\varphi(x_1,\ldots,x_n)$, and every $(g_1,\ldots,g_n)\in G^n$, \[ G\models\varphi(g_1,\ldots,g_n) \quad\Longleftrightarrow\quad H\models\varphi(\iota(g_1),\ldots,\iota(g_n)). \] The universal-existential fragment consists of formulas in universal-existential prenex form with quantifier-free matrix. Equality of universal-existential theories tests only sentences in this fragment; elementary equivalence tests all first-order sentences.

An HNN extension of a group $V$ over finite subgroups $A,B\leq V$, with an isomorphism $\theta:A\to B$, has the presentation \[ \left\langle V,t\ \middle|\ t^{-1}at=\theta(a)\text{ for every }a\in A\right\rangle. \] This definition does not specify the additional conditions denoted by legal large in the supplied record. Likewise, virtual cyclicity alone does not define a legal small replacement.

Conjecture as reported, with unresolved structural terminology. Extend the reported classifications and decision algorithms for the universal-existential fragment to unrestricted first-order formulas. The supplied expanded formulation asks for the following:

1. For finitely generated virtually free groups $G,H$, characterize $G\equiv H$ by the existence of a common overgroup obtainable from each of $G$ and $H$ through a finite sequence of legal large HNN extensions over finite subgroups and legal small replacements of virtually cyclic subgroups.
2. Characterize elementary embeddings between the groups under consideration by iterated legal large extensions. An embedding-specific formulation must identify the initial group with its given image and specify how the resulting extension is identified with the target group.
3. Obtain the corresponding decision algorithms without restricting formula complexity, including an algorithm deciding, for two groups in the stated class, whether their full first-order theories are equal, and the intended algorithm concerning elementary embeddings.

The phrases legal large extension and legal small replacement, their admissibility conditions, and the precise scope of the referenced earlier results are not defined in the supplied record. Consequently, the structural assertions above retain the source terminology and cannot yet be treated as fully specified equivalences. The input representation and the exact elementary-embedding decision task are also unspecified. No additional hypotheses or exceptions, including possible restrictions involving virtually cyclic groups, are imposed here.

Short English statement

The reported conjecture asks whether structural classifications and decision algorithms for finitely generated virtually free groups extend from universal-existential formulas to all first-order formulas. It concerns both elementary equivalence and elementary embeddings. The supplied record omits the definitions of the permitted legal operations and some algorithmic details, so these parts require source clarification before a complete formal statement is possible.

Sources

• Supplied local UnsolvedMath registry record, permanent ID $30004362$, title Elementary-Theory Classification of Virtually Free Groups, source problem code catalogue entry, in the Oberwolfach Reports Open Problems collection. No individual proposer is supplied; the proposed year is recorded as 2020.
• Supplied report citation: Model Theory: Groups, Geometries and Combinatorics (2021), Oberwolfach Reports, pp. 91--142, DOI 10.4171/owr/2020/2. https://doi.org/10.4171/owr/2020/2. The background describes this report as documenting workshop discussions and open problems.
• André, On Tarski's problem for virtually free groups. https://arxiv.org/abs/1910.08464.
• André, Elementary subgroups of virtually free groups. https://arxiv.org/abs/1912.06388.
• Literature assessment dated exactly 2026-08-22: the supplied curation labels the problem open and reports that algorithms cover important quantifier fragments, including the universal-existential theory, while the conjectured unrestricted first-order classification is not established. This is supplied dated curation derived from the OWR material, not an independently verified literature assessment; its status and cited claims require independent verification.
• The registry labels the statement corrected_verified and reports that the official report was checked, with the conjecture following two structural characterizations and their decision algorithms. This is a supplied verification claim, not a claim of source consultation in preparing this draft. The original wording refers to "the stated results" and removing restrictions on formula complexity; the expanded wording supplies the structural interpretation reproduced above.