Syntax becomes executable numerical data
The paper starts with ordinary inductive syntax—terms and formulas—then gives those objects numerical representations. Once encoded, transformations of syntax can be simulated by arithmetic operations on codes, while Lean verifies the correspondence.
Where does the “runtime” enter?
Not merely when a number represents a formula. The runtime interpretation appears when encoded syntax can be decoded, transformed, re-encoded, and verified as part of an executable procedure.
See the dependency structure
Diagonalization depends on substitution. Arithmetic substitution depends on encoding and decoding. Encoding depends on inductively defined syntax. The paper is therefore a layered construction, not a collection of independent results.
Terms
Because this is inductive, every term is a finite syntax tree. Structural recursion is therefore available automatically as the natural way to define transformations.
Formulas
Formulas are built from terms and logical constructors. The same tree structure later makes recursive substitution possible.
The syntax tree is the first computational object
Before Gödel numbers appear, the syntax is already executable data. Lean's inductive definitions give a finite object that programs can traverse. Gödel encoding then supplies a second representation of that same structure.
Term → Nat
def godel : Term → Nat :=
Encodable.encode
The code is determined by syntactic structure.
Nat → Option Term
def decodeTerm : Nat → Option Term :=
Encodable.decode
Decoding is partial because an arbitrary natural number need not be a valid code.
Round-trip correctness
This is stronger than saying “we assigned numbers.” It establishes a machine-checked correspondence between the structural object and its code.
Structural substitution
Basic substitution law
Why recursion appears naturally
The definition follows the constructors of the term. A variable is inspected directly; successor recurses into one child; addition recurses into both children.
Code-level substitution
The paper's central computational move is to perform syntactic substitution through numerical representations.
Theorem 5.2
= godelF(substFormula(x,s,φ))
Two representations, one transformation
The left side performs the operation through codes. The right side performs it structurally and then encodes. Their equality is the verified bridge between arithmetic and syntax.
Why diagonalization needs everything before it
A formula can only be made to refer to its own code after syntax can be encoded and substitution can be represented arithmetically.
Theorem 6.1
For every formula with one free variable, a sentence exists that says of itself what φ says of its code.
Choose φ(x) := ¬Prov(x)
This produces the familiar self-referential sentence: G says that G is not provable.
Main results
Click each theorem to see what it depends on and what it enables.
enables distinct syntax has distinct numerical representation.
enables verified recovery of syntax from its valid code.
enables confidence that the structural operation has the intended variable-replacement behavior.
enables arithmetic operations on codes to simulate syntactic transformation.
enables construction of self-referential sentences.
enables the paper's transition from executable self-reference to the classical incompleteness discussion.
Gödel runtime representation
The paper abstracts the construction into three ingredients:
The third ingredient is decisive: operations on codes must simulate structural transformations on the original expressions.
Syntax as executable data
Substitution, rewriting, normalization, and related compiler transformations can be understood as operations over encoded logical structures, with Lean supplying correctness proofs.
Representation becomes infrastructure
The paper's software interpretation is that the encoding is a runtime layer connecting symbolic rules to verified executable transformations.
What is the invariant being preserved?
At each layer, the same syntactic meaning is represented differently: first as a tree, then as a number, then as a transformed number, and finally again as syntax. The correctness theorems certify that the numerical computation agrees with the intended structural computation. That viewpoint is a useful doorway into the later idea of semantic invariance.