Axiomatizable classes of groups

AbbreviationClass of groups#✓fully proved

A class of groups, as a predicate on groups in Type.

abbrev GroupClass : Type 1 := ∀ (G : Type) [Group G], Prop

Used by 4

Used byThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32) · First-order axiomatizable classes of groups · Formations of groups in the sense of Gaglione and Spellman · Varieties of groups

DefinitionFormations of groups in the sense of Gaglione and Spellman#✓fully proved

A class \(\mathfrak{F}\) of groups is a formation when it contains at least one group, it is closed under surjective homomorphic images (if \(G \in \mathfrak{F}\) and \(\varphi \colon G \to H\) is a surjective homomorphism, then \(H \in \mathfrak{F}\)), and for every group \(G\) and all normal subgroups \(N_1\), \(N_2\) of \(G\), if \(G/N_1\) and \(G/N_2\) lie in \(\mathfrak{F}\), then so does \(G/(N_1 \cap N_2)\).

Together with closure under homomorphic images, the last condition amounts to closure under subdirect products of finitely many factors; the groups need not be finite.

def IsFormation (𝔉 : GroupClass) : Prop :=
  (∃ (G : Type) (_ : Group G), 𝔉 G) ∧
    (∀ (G H : Type) [Group G] [Group H] (φ : G →* H), Function.Surjective φ → 𝔉 G → 𝔉 H) ∧
    ∀ (G : Type) [Group G] (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal],
      𝔉 (G ⧸ N₁) → 𝔉 (G ⧸ N₂) → 𝔉 (G ⧸ (N₁ ⊓ N₂))

Uses 1 · Used by 1

Statement usesClass of groups

Used byThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32)

DefinitionFirst-order axiomatizable classes of groups#✓fully proved

A class \(\mathfrak{F}\) of groups is first-order axiomatizable when there is a theory \(T\) in the first-order language of groups such that a group \(G\) lies in \(\mathfrak{F}\) if and only if \(G\), with its canonical structure, is a model of \(T\).

def IsAxiomatizable (𝔉 : GroupClass) : Prop :=
  ∃ T : groupLanguage.Theory, ∀ (G : Type) [Group G],
    𝔉 G ↔ @Theory.Model groupLanguage G (groupLanguageStructure G) T

Uses 3 · Used by 1

Statement usesThe first-order language of groups · The canonical structure on a group · Class of groups

Used byThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32)

DefinitionVarieties of groups#✓fully proved

A class \(\mathfrak{F}\) of groups is a variety when there is a set \(W\) of elements of the free group on generators \(x_0, x_1, x_2, \dots\) such that a group \(G\) lies in \(\mathfrak{F}\) if and only if every \(w \in W\) evaluates to \(1\) in \(G\) under every assignment of elements of \(G\) to the generators.

def IsVariety (𝔉 : GroupClass) : Prop :=
  ∃ W : Set (FreeGroup ℕ), ∀ (G : Type) [Group G],
    𝔉 G ↔ ∀ w ∈ W, ∀ x : ℕ → G, FreeGroup.lift x w = 1

Uses 1 · Used by 1

Statement usesClass of groups

Used byThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32)

DefinitionThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32)#✓fully proved

The proposition that every first-order axiomatizable formation of groups is a variety: every class \(\mathfrak{F}\) of groups that is a formation and is first-order axiomatizable is a variety.

def axiomatizableFormationIsVariety : Prop :=
  ∀ 𝔉 : GroupClass, IsFormation 𝔉 → IsAxiomatizable 𝔉 → IsVariety 𝔉

Uses 4 · Used by 1

Statement usesClass of groups · First-order axiomatizable classes of groups · Formations of groups in the sense of Gaglione and Spellman · Varieties of groups

Used byNot every axiomatizable formation of groups is a variety

TheoremNot every axiomatizable formation of groups is a variety#●ready to prove

The Gaglione–Spellman question (Kourovka 14.32) has a negative answer: it is not the case that every first-order axiomatizable formation of groups is a variety, that is, some class of groups is a formation and is first-order axiomatizable but is not a variety.

Kearnes proved more: every variety of groups that contains a finite non-solvable group contains a first-order axiomatizable subformation that is not a variety.

public theorem_wanted axiomatizableFormationIsVariety_refuted : ¬ axiomatizableFormationIsVariety

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 14.32 (A. M. Gaglione, D. Spellman); resolution: K. A. Kearnes, J. Group Theory 13 (2010), no. 2, 233-241, Kourovka Archive, Problem 14.32: every variety of groups containing a finite non-solvable member contains an axiomatic subformation that is not a variety (answer: No).

Uses 1

Statement usesThe Gaglione–Spellman question on axiomatizable formations (Kourovka 14.32)

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.