Kourovka 1.20

### What is the conjecture
The question is **Problem 1.20** from the **Kourovka Notebook** (Unsolved Problems in Group Theory), posed by **Yu. L. Ershov** in the first issue (1965).

The problem asks: **"For which groups (classes of groups) is the lattice of normal subgroups first order definable in the lattice of all subgroups?"**

The question is discussed in research papers, primarily in the context of **lattice characterizations of groups** and **model theoretic properties of subgroup lattices**. However, as of the latest editions of the Kourovka Notebook (including the 20th edition and drafts for the 21st), the problem remains listed as **unsolved** in its full generality.

Here are the key details regarding the status and discussion of this question:

1. **Status of the Problem:**
* It is considered an **open problem** for the general class of all groups.
* Unlike the preceding Problem 1.19 (also by Ershov, regarding definable subgroups in free groups), which was marked as solved (by O. Kharlampovich and A. Myasnikov in 2013), Problem 1.20 does not have a comprehensive solution that covers all group classes.

2. **Known Partial Results & Trivial Cases:**
* **Abelian Groups (and Dedekind Groups):** For groups where every subgroup is normal (Dedekind groups), the lattice of normal subgroups $N(G)$ coincides with the lattice of all subgroups $L(G)$. In this case, the predicate "$\,H$ is a normal subgroup" is trivially definable (it is true for all elements).
* **Simple Groups:** For a simple group $G$, the lattice of normal subgroups consists only of the bottom element (trivial subgroup) and the top element ($G$ itself). These are always first-order definable in $L(G)$ as the unique minimal and maximal elements.
* **Projectivities:** The property of "being a normal subgroup" is **not** a lattice-theoretic property in general. That is, there exist groups $G$ and $H$ with isomorphic subgroup lattices ($L(G) \cong L(H)$) where a normal subgroup in $G$ corresponds to a non-normal subgroup in $H$. This implies that no formula in the first-order language of lattices can define normal subgroups for *all* groups. The problem asks specifically for *which* classes of groups such a formula exists.

3. **Relevant Literature:**
* The problem is frequently cited in literature dealing with the **model theory of groups** and **subgroup lattice theory**.
* Standard references discussing the relationship between $N(G)$ and $L(G)$ include Roland Schmidt's book **"Subgroup Lattices of Groups"** (1994), which explores which properties of a group are determined by its subgroup lattice.
* Papers by authors such as **P. P. Pálfy**, **M. Suzuki**, and **G. Zacher** discuss lattice characterizations that are closely related to the definability of structure.

In summary, while the question is widely recognized and discussed in the context of group theory problems, a complete characterization of the classes of groups for which the normal subgroup lattice is first-order definable in the subgroup lattice has not yet been found.

### Prerequisites needed
Note: The following is by Gemini, so double-check.

Based on the current state of **Lean 4 Mathlib**, the necessary definitions and structures to **state** Kourovka Problem 1.20 are largely present. You do not need to define new mathematical structures from scratch, but you would need to "glue" existing components together, particularly from the Model Theory library.

The problem can be stated using the `Mathlib.ModelTheory` and `Mathlib.GroupTheory` libraries.

### Missing or "Glue" Definitions
While the core definitions exist, you would likely need to define the following specific instances or convenience wrappers which are not pre-bundled:

1. **The Algebraic Language of Lattices (Optional):**
Mathlib defines `FirstOrder.Language.order` (the language $L_{\le} = \{\le\}$). It does not seemingly have a pre-defined `FirstOrder.Language.lattice` (the language $L_{alg} = \{\sqcap, \sqcup\}$).
* *Context:* In lattice theory, definability is often discussed in terms of operations. However, since the subgroup lattice is a lattice, the relational language $\{\le\}$ and the algebraic language $\{\sqcap, \sqcup\}$ are inter-definable. You can state the question using `FirstOrder.Language.order` without loss of generality.

2. **Model Instance for Subgroups:**
You need to explicitly declare that `Subgroup G` is a structure over the language of orders.
* *Existing Component:* `Subgroup G` has a `CompleteLattice` instance (and thus `PartialOrder`).
* *Glue Needed:* You must invoke `FirstOrder.Language.orderStructure` to view the type `Subgroup G` as a model of first-order logic.

3. **Definability with Empty Parameters:**
Mathlib's `Set.Definable` predicate generally takes a set of parameters $A$. You would need to specify that the set of normal subgroups is definable with **empty parameters** ($A = \emptyset$), sometimes called "0-definable" or "absolute definability".

### How to State it in Lean 4
Here is how you would construct the statement using existing Mathlib definitions.

```lean
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.Subgroup.Lattice
import Mathlib.ModelTheory.Definability
import Mathlib.ModelTheory.Order

open FirstOrder FirstOrder.Language

variable (G : Type*) [Group G]

-- 1. Establish the Language and Structure
-- We use the language of order {≤}, which is standard for subgroup lattices.
-- We automatically get an `OrderedStructure` instance for `Subgroup G`
-- because it already has a `PartialOrder` instance.
instance : Structure Language.order (Subgroup G) :=
Language.orderStructure (Subgroup G)

-- 2. Define the target set: The set of Normal Subgroups
def normalSubgroupsSet : Set (Subgroup G) := { H | H.Normal }

-- 3. The Statement: Is this set First-Order Definable?
-- We use `Set.Definable` with an empty set of parameters (∅).
def IsNormalLatticeDefinable : Prop :=
Set.Definable Language.order (normalSubgroupsSet G) (∅ : Set (Subgroup G))

-- 4. The Kourovka Question (Formalized as a predicate on Group classes)
-- "For which classes of groups..." can be modeled as finding a predicate P.
-- This example asks if a specific class P has the property.
def KourovkaProblem1_20 (P : Type* → Prop) : Prop :=
∀ (G : Type*) [Group G], P G → IsNormalLatticeDefinable G
```

### Summary of Coverage
* **Groups/Subgroups:** ✅ Covered (`Mathlib.GroupTheory`). `Subgroup G` is a `CompleteLattice`.
* **Normal Subgroups:** ✅ Covered. `Subgroup.Normal` is a predicate.
* **First-Order Logic:** ✅ Covered (`Mathlib.ModelTheory`). Definitions for `Language`, `Structure`, and `Formula` exist.
* **Definability:** ✅ Covered (`Mathlib.ModelTheory.Definability`). The predicate `Set.Definable` allows you to state that a subset of a model is defined by a formula.

**Conclusion:** No fundamental definitions are missing. The primary task is simply importing the correct modules and instantiating the model-theoretic structure for `Subgroup G`.

### [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 imports and definitions in Mathlib.ModelTheory.Definability, Mathlib.ModelTheory.Order, and the subgroup lattice modules; the issue provides no repository file or test entry point. Verify that the suggested statement compiles, then formalize the conjecture with an appropriate definability predicate and add the corresponding project entry.

Written by the indexing model from the issue text.