Decidability.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 0 contain sorry, 0 declared as axioms

Recursive and decidable theories

Mathlib's FirstOrder.Language.Theory is an arbitrary set of sentences, which need not be closed under logical consequence. Two computability notions are therefore distinct:

T is recursive if membership in T is computable: there is an algorithm which, given a sentence φ, decides whether φ ∈ T. This is a property of the set of axioms.
T is decidable if the set of consequences {φ | T ⊨ᵇ φ} is recursive: there is an algorithm which decides whether φ holds in every model of T. This only depends on the consequences of T, so it is invariant under replacing T by a logically equivalent set of axioms (FirstOrder.Language.Theory.isDecidable_congr).

The two notions agree when T is closed under consequence, in particular for the complete theory L.completeTheory M of a structure M (FirstOrder.Language.Theory.isDecidable_completeTheory_iff).

Both notions use the Gödel numbering of sentences from FormalConjecturesForMathlib.ModelTheory.Encoding and the notion of a computable function ℕ → Bool from Mathlib's computability library. As usual, they are relative to the chosen encoding of the symbols of L. For a language with finitely many symbols, all injective encodings of the symbols give the same notions.

Main declarations

FirstOrder.Language.Theory.IsRecursive: membership in the set of sentences is computable.
FirstOrder.Language.Theory.IsDecidable: the set of consequences is recursive.
FirstOrder.Language.Theory.isDecidable_iff_isRecursive: for a theory closed under consequence, the two notions agree.

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

def FirstOrder.Language.Theory.IsRecursive Documented declaration: IsRecursive line 61 source
Source documentation
A set of sentences T is recursive if there is a computable function f : ℕ → Bool such that, for every sentence φ, f returns true on the Gödel number of φ if and only if φ ∈ T.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory
Proof uses: Exists, Bool, And, Computable, FirstOrder.Language.Sentence, Iff, Eq, Encodable.encode, Empty, OfNat.ofNat, Bool.true, Membership.mem
8 instances, coercions and auxiliary constants left out.
```
def IsRecursive (T : L.Theory) : Prop :=
…
```
def FirstOrder.Language.Theory.IsDecidable Documented declaration: IsDecidable line 67 source
Source documentation
A theory T is decidable if the set of its consequences {φ | T ⊨ᵇ φ} is recursive: there is an algorithm which, given a sentence φ, decides whether φ holds in every model of T.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory
Proof uses: FirstOrder.Language.Theory.IsRecursive, Set.ofPred, FirstOrder.Language.Sentence, FirstOrder.Language.Theory.ModelsBoundedFormula, Empty, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def IsDecidable (T : L.Theory) : Prop :=
…
```
theorem FirstOrder.Language.Theory.isRecursive_empty The empty set of sentences is recursive line 73 source
Source documentation
The empty set of sentences is recursive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory.IsRecursive, EmptyCollection.emptyCollection, FirstOrder.Language.Theory, FirstOrder.Language.Sentence
Proof uses: Exists.intro, Bool, And, Computable, Iff, Eq, Encodable.encode, Empty, OfNat.ofNat, Bool.true, Membership.mem, Bool.false, And.intro, Computable.const, of_eq_true, Eq.trans, False, True, congr, congrArg and 2 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isRecursive_empty : (∅ : L.Theory).IsRecursive :=
…
```
Mentions: FirstOrder.Language.Theory.IsRecursive
theorem FirstOrder.Language.Theory.isRecursive_univ The set of all sentences is recursive line 77 source
Source documentation
The set of all sentences is recursive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory.IsRecursive, Set.univ, FirstOrder.Language.Sentence
Proof uses: Exists.intro, Bool, And, Computable, Iff, Eq, Encodable.encode, Empty, OfNat.ofNat, Bool.true, Membership.mem, FirstOrder.Language.Theory, And.intro, Computable.const, of_eq_true, Eq.trans, True, congr, congrArg, eq_self and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isRecursive_univ : IsRecursive (Set.univ : L.Theory) :=
…
```
Mentions: FirstOrder.Language.Theory.IsRecursive
theorem FirstOrder.Language.Theory.IsRecursive.compl The complement of a recursive set of sentences is recursive line 81 source
Source documentation
The complement of a recursive set of sentences is recursive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory, FirstOrder.Language.Theory.IsRecursive, Compl.compl, FirstOrder.Language.Sentence
Proof uses: Bool, And, Computable, Iff, Eq, Encodable.encode, Empty, OfNat.ofNat, Bool.true, Membership.mem, Exists.intro, Bool.not, And.intro, Computable.of_eq, cond, Bool.false, Computable.cond, Computable.const, Eq.refl, Eq.symm and 22 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem IsRecursive.compl (hT : T.IsRecursive) : Tᶜ.IsRecursive := by
…
```
theorem FirstOrder.Language.Theory.isDecidable_congr Decidability only depends on the consequences of a theory line 93 source
Source documentation
Decidability only depends on the consequences of a theory. In particular, logically equivalent sets of axioms are decidable together.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory, FirstOrder.Language.Sentence, Iff, FirstOrder.Language.Theory.ModelsBoundedFormula, Empty, OfNat.ofNat, FirstOrder.Language.Theory.IsDecidable
Proof uses: id, Eq.mpr, FirstOrder.Language.Theory.IsRecursive, Set.ofPred, FirstOrder.Language.BoundedFormula, Eq, congrArg, Set, Set.ext, Iff.rfl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isDecidable_congr (h : ∀ φ : L.Sentence, T ⊨ᵇ φ ↔ T' ⊨ᵇ φ) :
    T.IsDecidable ↔ T'.IsDecidable := by
…
```
theorem FirstOrder.Language.Theory.isDecidable_iff_isRecursive For a theory closed under consequence, decidability is the same as recursiveness line 99 source
Source documentation
For a theory closed under consequence, decidability is the same as recursiveness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory, FirstOrder.Language.Sentence, FirstOrder.Language.Theory.ModelsBoundedFormula, Empty, OfNat.ofNat, Membership.mem, Iff, FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.Theory.IsRecursive
Proof uses: id, Eq.mpr, Set.ofPred, Eq, congrArg, Set, Set.ext, Iff.intro, FirstOrder.Language.Theory.models_sentence_of_mem, Iff.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isDecidable_iff_isRecursive (hT : ∀ φ : L.Sentence, T ⊨ᵇ φ → φ ∈ T) :
    T.IsDecidable ↔ T.IsRecursive := by
…
```
theorem FirstOrder.Language.Theory.isDecidable_completeTheory_iff The complete theory of a structure M contains all its consequences, so it is decidable if and only if membership in it is computable line 106 source
Source documentation
The complete theory of a structure M contains all its consequences, so it is decidable if and only if membership in it is computable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Structure, Nonempty, Iff, FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.completeTheory, FirstOrder.Language.Theory.IsRecursive
Proof uses: FirstOrder.Language.Theory.isDecidable_iff_isRecursive, FirstOrder.Language.Sentence, FirstOrder.Language.Theory.ModelsBoundedFormula, Empty, OfNat.ofNat, Iff.mpr, Membership.mem, FirstOrder.Language.Theory, FirstOrder.Language.Sentence.Realize, FirstOrder.Language.mem_completeTheory, FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence
3 instances, coercions and auxiliary constants left out.
```
theorem isDecidable_completeTheory_iff (M : Type*) [L.Structure M] [Nonempty M] :
    (L.completeTheory M).IsDecidable ↔ (L.completeTheory M).IsRecursive :=
…
```
Mentions: FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.Theory.IsRecursive
theorem FirstOrder.Language.Theory.isDecidable_univ The inconsistent theory of all sentences is decidable line 111 source
Source documentation
The inconsistent theory of all sentences is decidable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.Relations, FirstOrder.Language.Theory.IsDecidable, Set.univ, FirstOrder.Language.Sentence
Proof uses: Iff.mpr, FirstOrder.Language.Theory.IsRecursive, FirstOrder.Language.Theory.isDecidable_iff_isRecursive, FirstOrder.Language.Theory.ModelsBoundedFormula, Empty, OfNat.ofNat, Set.mem_univ, FirstOrder.Language.Theory.isRecursive_univ
1 instances, coercions and auxiliary constants left out.
```
theorem isDecidable_univ : IsDecidable (Set.univ : L.Theory) :=
…
```
Mentions: FirstOrder.Language.Theory.IsDecidable