Modal group theory: homomorphisms

Referee: [proof of the main isomorphism theorem] The central claim (computable isomorphism between the homomorphic modal theory of all f.p. groups and true arithmetic) is load-bearing on validity in the trivial group, which is finitely presented. In the trivial group the only homomorphism is the identity, so □φ and ◇φ both reduce to φ itself. The abstract separates the trivial-group case for parameter-validities (exactly S5), but it is unclear how an arbitrary arithmetic sentence ψ is encoded as a modal sentence φ_ψ such that φ_ψ is valid in the trivial group precisely when ψ is true, while failing in some other f.p. group when ψ is false. This encoding must be verified explicitly in the proof of the isomorphism.

Authors: The encoding of an arbitrary arithmetic sentence ψ as a modal sentence φ_ψ is constructed explicitly in the proof of Theorem 4.3 (Section 4). The construction proceeds by induction on the complexity of ψ, using the modal formulas from Section 3 that define the arithmetic predicates (addition, multiplication, etc.) inside groups. In the trivial group, the modal operators reduce to the identity, so φ_ψ holds precisely when the interpreted arithmetic sentence ψ holds, which occurs exactly when ψ is true. When ψ is false, the inductive construction produces a specific finitely presented group G (typically a suitable non-abelian free group or a finite presentation in which the arithmetic relations fail) together with a homomorphism from G to a quotient in which the corresponding modal formula is falsified. The two directions of the equivalence are verified in full detail in the proof. revision: partial

Referee: [definability section] The definability results for cyclicity and torsion (used to interpret arithmetic) must hold uniformly, including under homomorphisms that collapse the group. The semantics permits identification of elements and killing of parameters; it is not immediate that the modal formulas distinguish cyclic from non-cyclic groups or detect torsion without additional restrictions on the class of groups or the language. A concrete verification that the defining formulas remain faithful after collapse would be required.

Authors: The definability theorems in Section 3 are stated and proved for arbitrary groups and arbitrary homomorphisms. Each proof proceeds by showing that the modal formula holds in a group G if and only if the corresponding group-theoretic property holds in G, with the argument relying only on the existence of homomorphisms and therefore remaining valid when elements are identified or parameters are killed. We will add a short subsection containing two explicit examples (one collapsing homomorphism that preserves cyclicity and one that detects torsion) to make the uniformity fully concrete. revision: yes