15 August 2026

Gödel and Lean: can we discuss formal language inside a formal language?

Lean is both a programming language and a theorem prover [4]. That makes it a natural place to ask a slightly strange question: can we use one formal language to define another formal language, talk about proofs in that language, and then construct a sentence which, in some sense, talks about its own provability?

This is the same idea that Gödel had around 1930, before publishing his historical paper in 1931. What followed was perhaps one of most elegant and beautiful theorems of mathematics, Gödel's incompleteness theorems [1]. A full formalization of his formalization is a serious endeavour: one needs an arithmetic theory, a coding of formulas and proofs by natural numbers, a formal proof predicate, substitution, representability results, and the diagonal lemma. Instead of reproducing all of that here, I want to build a deliberately small Lean model which captures the shape of diagonalization while being very explicit about what it leaves out.

The result is not a full reproduction of Gödel's construction. It is a model of one of its central mechanisms: constructing a formula G whose interpretation satisfies G ↔ ¬Provable(G).

More detail: what Gödel's theorem is actually about

Gödel's first incompleteness theorem concerns sufficiently expressive, effectively axiomatized formal theories. Very roughly, it states that a consistent, effectively axiomatized formal theory capable of expressing enough arithmetic is necessarily incomplete. Modern presentations such as [6] [7] often use the diagonal lemma: for a formula A(x) with one free variable, one can construct a sentence D such that the theory proves D ↔ A(⌜D⌝), where ⌜D⌝ denotes a numerical code for the syntax of D. There is no single definition of a numerical code. The original construction in Gödel used prime number decomposition to encode symbols into numerical codes, and then into exponents for successive prime number.

The Stanford Encyclopedia of Philosophy gives exactly this formulation of the diagonalization lemma and emphasizes the crucial point that codification is provable equivalence. Its supplement on diagonalization explains the key operation in terms of substitution on Gödel codes.

For incompleteness, we eventually need to choose a property such as A(x) := ¬Prov(x) where x is a numerical code representing a statement in its own formal theory. The resulting fixed point (that is, an application of the predicate to its own code) behaves like:

G ↔ ¬Prov(⌜G⌝)

Informally, we say that the Gödel sentence G "states that it itself is not provable". This phrasing is useful, but it should not be confused with the contradiction L ↔ ¬L. Gödel's construction concerns provability in a specified formal system, and is not a direct negation of the sentence itself.

Lean lets us build a language as data

Lean is well suited to this experiment because we can represent the syntax of another language using inductive datatypes. This is standard Lean code: its documentation introduces inductive types as the basic mechanism for constructing recursive datatypes, and its propositions-and-proofs chapter explains how logical propositions themselves live inside Lean's dependent type theory.

The first distinction to keep clear is therefore the one between Lean, which is the host language (metatheory), and our formula, which is the syntax of a tiny, toy language which is encoded inside Lean.

Our toy language will be intentionally tiny. It contains only falsehood, implication, and a predicate intended to mean "the formula represented by this term is provable". Negation does not need to be primitive, since ¬P can be represented as P → ⊥, where ⊥ is the falsehood symbol.

namespace MiniGodel

mutual
  inductive Term : Type where
    | var   : Term
    | quote : Formula → Term
    | diag  : Term → Term

  inductive Formula : Type where
    | bot  : Formula
    | imp  : Formula → Formula → Formula
    | prov : Term → Formula
end

open Term Formula

def negF (p : Formula) : Formula :=
  .imp p .bot

This already contains the biggest shortcut that we will take in this article: quote and diag are primitive constructors in our toy syntax. In any exhaustive Gödel proof, they would not be free operations and would need a lengthy formalization. Formulas and proofs are encoded by natural numbers in the Gödel construction, and one has to show that the relevant operations on those codes are arithmetically representable.

What does "diagonalization" mean?

Suppose we have a formula with one free variable:

A(x)

Think of x as a slot into which we can place the numerical code of a formula, almost like a function, except this is just an effective syntactic operation. If we can mechanically substitute a formula's own code into such a slot, we can create a fixed point construction.

The characteristic construction is:

start with A(x)
build a template δ(x)
then form δ(⌜δ⌝)

The clever part is arranging our predicate δ so that the code produced inside it refers to the final sentence. The diagonal lemma guarantees that this can be done in sufficiently strong arithmetical theories. Their strongness is the weakness that makes it possible for admissible statements to be unprovable inside said theory.

In our toy Lean model, We will not prove that arithmetic can perform this coding. We implement the operation directly. First, substitution replaces the free syntax variable by another term:

mutual
  def substTerm (replacement : Term) : Term → Term
    | .var       => replacement
    | .quote f   => .quote f
    | .diag t    => .diag (substTerm replacement t)

  def substFormula (replacement : Term) : Formula → Formula
    | .bot       => .bot
    | .imp p q   =>
        .imp
          (substFormula replacement p)
          (substFormula replacement q)
    | .prov t    =>
        .prov (substTerm replacement t)
end

Notice that substitution does not enter quote f. Quoted syntax is treated as data. This is analogous to the difference between a variable in a program and the same characters appearing freely inside a string literal.

Now we give our terms an interpretation. The interesting case is that of diag:

def evalTerm (ρ : Formula) : Term → Formula
  | .var =>
      ρ

  | .quote f =>
      f

  | .diag t =>
      let f := evalTerm ρ t
      substFormula (.quote f) f

This definition is the toy version of diagonalization. It is simple enough to be clear, and at the same time gives the full picture. Given a term denoting a formula f, it replaces the free variable of f by the quotation (a numeric code in the original, in this implementation a syntax tree) of f itself.

In informal notation:

diag(⌜f⌝)  ↦  f(⌜f⌝)

That is the self-application step. Again, in a real incompleteness proof this operation is encoded as arithmetic on natural numbers. Here Lean simply computes it on syntax trees internally.

Building the Gödel-shaped sentence

Next we give our formulas a semantics. The meaning of Prov(t) is supplied by an external Lean predicate Provable : Formula -> Prop:

def Holds
    (Provable : Formula → Prop)
    (ρ : Formula) :
    Formula → Prop
  | .bot =>
      False

  | .imp p q =>
      Holds Provable ρ p →
      Holds Provable ρ q

  | .prov t =>
      Provable (evalTerm ρ t)

This is yet another major simplification to keep our discussion simple. In a genuine Gödel formalization, provability is itself arithmetized: one defines a relation such as Proof_T(p, n), meaning that p codes a valid proof in the theory T of the sentence coded by n, and then:

Prov_T(n) := ∃ p, Proof_T(p, n)

Note that while at first glance constructing such predicate seems incredibly complex, it is really not. The predicate does not create a proof for the statement itself, yet it simply verifies if all provided steps are correct. In any sufficiently formal theory, this just corresponds to repeated applications of the theory's axioms and induction patterns, which is easy to imagine mechanically. Our toy model skips that entire layer and lets Lean provide Provable from outside.

Now define the idea "this represented formula is not provable":

def psi : Formula :=
  negF (.prov .var)

Conceptually:

ψ(x) = ¬Prov(x)

We then make the diagonal template and get ready for diagonalization:

def delta : Formula :=
  negF (.prov (.diag .var))

so:

δ(x) = ¬Prov(diag(x))

Finally, we are ready to substitute the quotation of delta inside delta itself:

def G : Formula :=
  substFormula (.quote delta) delta

Inside Lean, we can reduce the resulting syntax:

theorem G_shape :
    G =
      .imp
        (.prov (.diag (.quote delta)))
        .bot := by
  rfl

The crucial computation is that diag(quote delta) denotes G:

theorem diagonal_points_to_G (ρ : Formula) :
    evalTerm ρ (.diag (.quote delta)) = G := by
  rfl

Therefore, under our semantics, G has exactly the fixed-point property we wanted for our construction:

theorem godel_spec
    (Provable : Formula → Prop) :
    Holds Provable .bot G ↔
      ¬ Provable G := by
  rfl

Note that the fact that this proof is just rfl is not evidence that Gödel's theorem is trivial. It means that we deliberately designed the toy syntax and its diag operator so that the fixed-point equation is true by computation. The real genius and novelty in Gödel's construction is that he proves that ordinary arithmetic can encode enough syntax and computation to obtain the same effect without a built-in diag instruction. That effort alone is what makes him one of the greatest logicians to ever live.

Why is there no contradiction?

Our sentence has the form:

G ↔ ¬Provable(G)

It is important to note that the sentence does not have the form:

G ↔ ¬G

The distinction between truth and provability is the entire point of our construction. A statement can fail to have a proof in a particular theory without being false. This is the case for examples for the Axiom of Choice (AC): it can be shown that inside the very common Zermelo-Fraenkel set theory at the basis of modern real analysis, assuming ZF is consistent, adding AC does not create inconsistency, and similarly for the negation AC. Neither is a theorem of ZF.

If we additionally define a proof relation and assume that the proof system is sound for our semantics, then a proof of G would imply that G is true. But the truth condition for G says that G is not provable. So, under that soundness assumption, G cannot be proved.

assume Provable(G) ->
soundness
        ->
G
        ->
meaning of G
        ->
¬Provable(G) -> contradiction!

This is enough to illustrate the tension, but it is not the standard first incompleteness theorem in its full technical form. My small argument assumes semantic soundness, which is stronger and simpler than the hypotheses normally used in Gödel or Rosser incompleteness results.

What we have showed and what we did not

Our toy system makes the central syntactic operation primitive:

toy model                     full Gödel construction

Formula datatype          →   natural-number Gödel codes
quote φ                   →   numeral for ⌜φ⌝
diag                      →   encoded substitution function
Provable : Formula → Prop →   ∃ p, Proof_T(p, n)

The full theorem is remarkable because all the constructs that we took for granted were constructed using arithmetic itself.

So, can a formal language discuss a formal language?

The answer is yes, but there are several levels that should not be collapsed into one. We used Lean to define and reason about the syntax of a toy language, which contained expressions like Prov(t) which we interpret using a provability predicate.

Lean is not confused by this. From Lean's perspective, our formulas are ordinary inductive data. Functions such as substitution are ordinary recursive programs. Statements about those functions are ordinary propositions checked by Lean's kernel.

This host-language/object-language separation is one of the useful ways to understand formal logic. We can use a formal system as a metatheory in which we define another system, its syntax, its proof rules, and properties of those proof rules.

One can go substantially further. The lean4-logic project develops propositional and first-order logic, arithmetic, computability machinery, and formal incompleteness results in Lean. Its summary includes a formal first incompleteness theorem and an explicitly constructed undecidable sentence. That is much closer to the full right-hand column above than this article's miniature model.

There is an additional recursive-looking twist: implementations such as Lean4Lean implement a Lean 4 kernel checker largely in Lean 4 itself. That is a different problem from Gödel incompleteness, but it reinforces the same conceptual lesson: formal languages can represent and manipulate descriptions of formal languages, including languages closely related to themselves.

The theoretical lesson

The profound step in Gödel's argument is not the use of exotic logical connectives. In fact, our toy language needed very little propositional logic. The hard part is turning syntax into data and making operations on syntax available inside arithmetic.

Once formulas, substitutions, and proofs can be encoded by numbers, arithmetic can express statements about arithmetic proofs. Diagonalization then produces fixed points: sentences related, by a theorem of the formal system, to claims about their own codes.

That mechanism does not make the formal system explode in contradiction. Instead, under the relevant hypotheses, it exposes a gap between two notions that are easy to conflate: truth in the intended interpretation is not provability inside a particular formal theory

Our Lean model only sketches that boundary. But even the sketch is useful because every layer is explicit: syntax is a datatype, quotation is a constructor, substitution is a function, diagonalization is an operation, and the fixed-point property is a theorem that Lean checks.