Encoding.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

8 declarations, 0 contain sorry, 0 declared as axioms

Gödel numberings of first-order formulas

Mathlib encodes the terms and the bounded formulas of a first-order language L as lists of symbols (FirstOrder.Language.Term.listEncode and FirstOrder.Language.BoundedFormula.listEncode), and derives from this an Encodable instance on terms. This file derives Encodable instances on bounded formulas, formulas and sentences in the same way. Given Encodable instances on the function symbols Σ n, L.Functions n and on the relation symbols Σ n, L.Relations n, every sentence φ of L gets a Gödel number Encodable.encode φ : ℕ.

The file also provides Encodable instances on the symbols of Language.ring, Language.order, and of sums of languages.

Main declarations

FirstOrder.Language.BoundedFormula.encodableSigma: Gödel numbering of Σ n, L.BoundedFormula α n.
FirstOrder.Language.BoundedFormula.encodable: Gödel numbering of L.BoundedFormula α n, hence of L.Formula α and L.Sentence.

Implementation notes

The numbering is the composition of Mathlib's list encoding of formulas with Mathlib's Encodable instance on lists and the given encodings of the symbols, so it is effective in the usual informal sense. For a language with finitely many symbols, any two injective encodings of the symbols yield Gödel numberings that are computably inter-translatable, so notions such as decidability of a theory do not depend on the choice made here. No Primcodable instance is provided; computability statements about theories are phrased on ℕ through Encodable.encode.

Imports (3)

Imported by 3 files

instance FirstOrder.Language.sum.encodableFunctions The function symbols of a sum of two languages are encodable when those of both summands are line 65 source
Source documentation
The function symbols of a sum of two languages are encodable when those of both summands are.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.sum
Proof uses: Encodable.ofEquiv, Sum, Equiv.sigmaSumDistrib
1 instances, coercions and auxiliary constants left out.
```
instance sum.encodableFunctions {L' : Language} [Encodable (Σ n, L.Functions n)]
    [Encodable (Σ n, L'.Functions n)] : Encodable (Σ n, (L.sum L').Functions n) :=
…
```
instance FirstOrder.Language.sum.encodableRelations The relation symbols of a sum of two languages are encodable when those of both summands are line 71 source
Source documentation
The relation symbols of a sum of two languages are encodable when those of both summands are.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FirstOrder.Language, Encodable, Sigma, Nat, FirstOrder.Language.Relations, FirstOrder.Language.sum
Proof uses: Encodable.ofEquiv, Sum, Equiv.sigmaSumDistrib
1 instances, coercions and auxiliary constants left out.
```
instance sum.encodableRelations {L' : Language} [Encodable (Σ n, L.Relations n)]
    [Encodable (Σ n, L'.Relations n)] : Encodable (Σ n, (L.sum L').Relations n) :=
…
```
instance FirstOrder.Language.IsRelational.encodableFunctions A relational language has no function symbols line 76 source
Source documentation
A relational language has no function symbols.

no axioms what this means
Statement uses: FirstOrder.Language, FirstOrder.Language.IsRelational, Encodable, Sigma, Nat, FirstOrder.Language.Functions
Proof uses: Encodable.mk, isEmptyElim, Sigma.fst, Sigma.snd, Option.none
2 instances, coercions and auxiliary constants left out.
```
instance IsRelational.encodableFunctions [L.IsRelational] : Encodable (Σ n, L.Functions n) :=
…
```
instance FirstOrder.Language.IsAlgebraic.encodableRelations An algebraic language has no relation symbols line 80 source
Source documentation
An algebraic language has no relation symbols.

no axioms what this means
Statement uses: FirstOrder.Language, FirstOrder.Language.IsAlgebraic, Encodable, Sigma, Nat, FirstOrder.Language.Relations
Proof uses: Encodable.mk, isEmptyElim, Sigma.fst, Sigma.snd, Option.none
2 instances, coercions and auxiliary constants left out.
```
instance IsAlgebraic.encodableRelations [L.IsAlgebraic] : Encodable (Σ n, L.Relations n) :=
…
```
instance FirstOrder.Language.ring.encodableFunctions The function symbols +, *, -, 0, 1 of the language of rings are encoded as 0, 1, 2, 3, 4 line 85 source
Source documentation
The function symbols +, *, -, 0, 1 of the language of rings are encoded as 0, 1, 2, 3, 4.

standard axioms: Quot.sound, propext what this means
Statement uses: Encodable, Sigma, Nat, FirstOrder.Language.Functions, FirstOrder.Language.ring
Proof uses: Encodable.ofLeftInjection, FirstOrder.Language.ring.encodableFunctions.match_1, Unit, OfNat.ofNat, FirstOrder.Language.ring.encodableFunctions.match_2, Option, Option.some, Sigma.mk, FirstOrder.Ring.addFunc, FirstOrder.Ring.mulFunc, FirstOrder.Ring.negFunc, FirstOrder.Ring.zeroFunc, FirstOrder.Ring.oneFunc, Option.none
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance ring.encodableFunctions : Encodable (Σ n, Language.ring.Functions n) :=
…
```
instance FirstOrder.Language.order.encodableRelations The unique relation symbol ≤ of the language of orders is encoded as 0 line 103 source
Source documentation
The unique relation symbol ≤ of the language of orders is encoded as 0.

standard axioms: Quot.sound, propext what this means
Statement uses: Encodable, Sigma, Nat, FirstOrder.Language.Relations, FirstOrder.Language.order
Proof uses: Encodable.ofLeftInjection, OfNat.ofNat, Option.some, Inhabited.default
5 instances, coercions and auxiliary constants left out.
```
instance order.encodableRelations : Encodable (Σ n, Language.order.Relations n) :=
…
```
instance FirstOrder.Language.BoundedFormula.encodableSigma The Gödel numbering of bounded formulas, obtained from the list encoding BoundedFormula.encoding and the Encodable instances on lists and on the symbols line 115 source
Source documentation
The Gödel numbering of bounded formulas, obtained from the list encoding BoundedFormula.encoding and the Encodable instances on lists and on the symbols.

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.BoundedFormula
Proof uses: Encodable.ofLeftInjection, List, Sum, FirstOrder.Language.Term, Fin, Computability.Encoding.encode, FirstOrder.Language.BoundedFormula.encoding, Computability.Encoding.decode
7 instances, coercions and auxiliary constants left out.
```
instance encodableSigma : Encodable (Σ n, L.BoundedFormula α n) :=
…
```
instance FirstOrder.Language.BoundedFormula.encodable The Gödel numbering of bounded formulas with n bound variables, and in particular of formulas (n = 0) and sentences (n = 0 and α = Empty) line 121 source
Source documentation
The Gödel numbering of bounded formulas with n bound variables, and in particular of formulas (n = 0) and sentences (n = 0 and α = Empty).

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.BoundedFormula
Proof uses: Encodable.ofLeftInjection, Sigma.mk, dite, Option, Eq, Sigma.fst, Option.some, Eq.rec, Sigma.snd, Not, Option.none
3 instances, coercions and auxiliary constants left out.
```
instance encodable (n : ℕ) : Encodable (L.BoundedFormula α n) :=
…
```