Kourovka 1.27 - Axiomatization

### What is the conjecture
**"There exists a recursive set of universal axioms $\Gamma$ such that $\Gamma$ axiomatizes the universal theory of free groups,"**

Kourovka Notebook Problem **1.27** is a famous problem discussed extensively in mathematical research papers, particularly in the fields of **group theory** and **mathematical logic** (model theory).

The general problem "Describe the universal theory of free groups" (posed by M. I. Kargapolov in the 1960s) has been a central driver of research in geometric group theory and model theory for decades. It is directly related to the famous **Tarski Conjectures** about the elementary theory of free groups.

Key milestones in the research include:
* **G. S. Makanin (1984):** Proved that the universal theory of free groups is **decidable**. This was a massive breakthrough, providing an algorithm to determine if a system of equations has a solution in a free group.
* **Kharlampovich & Myasnikov** and **Z. Sela (2006):** Independently solved the Tarski Conjecture, proving that the full first-order theory of non-abelian free groups is decidable and that all non-abelian free groups share the same elementary theory.
* **Limit Groups (Fully Residually Free Groups):** Research has characterized the groups that share the same universal theory as free groups. These are known as **limit groups** (or $\exists$-free groups). The study of limit groups is a major area of modern research.

Problem 1.27 is a **classification** or **characterization** problem. It asks for a **description**, which can be interpreted in several ways, all of which go beyond simple existence:
* **Axiomatization:** Find a specific set of axioms (universal sentences) that generate all the universal truths of free groups.
* **Algebraic Characterization:** Describe the class of groups that satisfy this theory (i.e., "Which groups look like free groups from the perspective of universal sentences?"). As noted above, this part has been largely answered: they are the **limit groups**.
* **Decidability:** While asking for a decision algorithm (which Makanin provided) implies asking for the *existence* of an algorithm, the problem of "describing" the theory implies understanding its structure, not just knowing it is computable.

### Summary
The problem is not a simple "yes/no" existence question. It is a request to understand the logical structure of free groups. While the **decidability** (existence of an algorithm) was settled by Makanin, research continues into finding explicit **axiomatizations** and understanding the geometric properties of the groups (limit groups) that satisfy this theory.

### Prerequisites needed
Note: this is from Gemini, so double-check.

To state the axiomatization problem in Lean 4 (specifically using Mathlib), you have most of the necessary ingredients, but a few specific "bridge" definitions are likely missing or require significant "boilerplate" setup.

To formally state: **"There exists a recursive set of universal axioms $\Gamma$ such that $\Gamma$ axiomatizes the universal theory of free groups,"** you need to connect **Group Theory**, **Model Theory**, and **Computability Theory**.

Here is the breakdown of what is available and what is "missing" (or requires manual construction).

### 1. What is available in Mathlib
* **Free Groups:** `GroupTheory.FreeGroup` contains the definition of free groups.
* **First-Order Logic:** `ModelTheory.Syntax` and `ModelTheory.Semantics` (derived from the "Flypitch" project) provide `Formula`, `Sentence`, `Structure`, and satisfiability ($\models$).
* **The Language of Groups:** `ModelTheory.Language` allows defining the language $L = \{*, ^{-1}, 1\}$.
* **Computability:** `Computability.Basic` and `Computability.Language` define what it means for a set to be recursive (decidable).

### 2. What is "Missing" (The Friction Points)
To state the problem in a single readable theorem, you would need to fill these gaps:

1. **Syntactic Classification (`IsUniversal`):**
While Mathlib has hierarchy definitions (like $\Sigma_n$ and $\Pi_n$ formulas), you may need to manually define the predicate `IsUniversal φ` (equivalent to $\Pi_1$) for sentences if a convenient alias doesn't exist. You specifically need to restrict the axioms to be **universal sentences** (sentences of the form $\forall \vec{x}, \psi(\vec{x})$ where $\psi$ is quantifier-free).

2. **Computability of Formulas (Gödel Numbering):**
This is the biggest technical gap. To say "The set of axioms is **recursive**," you need to apply computability theory to the type `Sentence L_grp`.
* *Missing:* An explicit instance that makes `Sentence L_grp` a computable type (i.e., a canonical way to encode formulas into natural numbers/Turing machine tapes). You would likely need to define a `ComputableEncoding` for first-order formulas to use predicates like `IsComputableSet`.

3. **The "Universal Theory" wrapper:**
You need to define the object $Th_{\forall}(F_2)$. Mathlib has `Theory` (set of all true sentences), but you need to filter this set to only include universal sentences.

### 3. Formal Statement in Lean 4

Here is how you would state the problem in Lean 4, including the "dummy" definitions you would need to implement to bridge the gaps.

```lean
import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Semantics
import Mathlib.GroupTheory.FreeGroup
import Mathlib.Computability.Language

open FirstOrder ModelTheory

-- 1. DEFINE THE LANGUAGE OF GROUPS
-- Mathlib has general languages, we specialize to groups (*, ⁻¹, 1)
-- (This is usually available or trivial to define)
def L_grp : Language := Language.group

-- 2. "MISSING" BRIDGE: CLASSIFYING UNIVERSAL FORMULAS
-- We need a predicate stating a sentence is ∀x, φ(x) (quantifier-free)
-- Mathlib tracks complexity, but we define a helper wrapper here.
def IsUniversal (φ : L_grp.Sentence) : Prop :=
φ.Complexity ≤ 1 -- Simplification: roughly corresponds to Π₁

-- 3. "MISSING" BRIDGE: COMPUTABILITY OF FORMULAS
-- We need to treat sentences as data that can be computed on.
-- We assume an encoding exists (Gödel numbering).
variable (enc : ComputableEncoding L_grp.Sentence)

-- 4. DEFINE THE OBJECT: FREE GROUPS
-- We stick to the Free Group on 2 generators (F₂), as all non-abelian
-- free groups share the same universal theory.
abbrev F2 := FreeGroup (Fin 2)

-- 5. THE PROBLEM STATEMENT
-- "Describe the universal theory" is interpreted as:
-- "Does there exist a recursive set of universal axioms that generates the theory?"

theorem Kourovka_1_27_Existence_of_Axiomatization :
∃ (Γ : Set L_grp.Sentence),
-- Condition A: The axioms are recursive (decidable membership)
-- (This requires the encoding 'enc' assumed above)
IsDecidablePred (λ φ => φ ∈ Γ) ∧

-- Condition B: The axioms are universal sentences
(∀ φ ∈ Γ, IsUniversal φ) ∧

-- Condition C: Γ axiomatizes the universal theory of F₂
-- i.e., For any universal ψ, F₂ ⊨ ψ iff Γ ⊢ ψ
(∀ (ψ : L_grp.Sentence), IsUniversal ψ →
(F2 ⊨ ψ ↔ Γ ⊢ ψ)) :=
sorry
```

### Summary of what is needed to complete the formalization:
1. **`Language.group`**: Ensure the standard language of groups is imported.
2. **`IsUniversal`**: A definition checking that a formula is in the $\Pi_1$ class (starts with universal quantifiers, no existential ones).
3. **`ComputableEncoding`**: A proof that the type `Sentence` is countable and encodable (essential for the "recursive" part of the problem).

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by checking the proposed Mathlib imports and whether Language.group, Sentence, Theory, and the computability interfaces exist as described. Then assess the missing IsUniversal classification, sentence encoding, and universal theory definitions. Done would require a validated Lean statement with the necessary bridge definitions, not just the current placeholder theorem.

Written by the indexing model from the issue text.