The Goedel numbering of first-order formulas is injective

Identifier: F:fo-formula-code-injective
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

FO.Formula.code assigns to every first-order formula a natural number -- FO.Code.pair tag payload, one distinct tag for each of the nine constructors, with FO.Term fields coded through FO.Term.code and the payload nesting to the right -- and the assignment is injective: if two formulas have the same code they are the same formula.

Formal statement

theorem FO.Formula.code_injective : ((x0 : FO.Formula) -> ((x1 : FO.Formula) -> ((x2 : Eq.{1} AxNat (FO.Formula.code x0) (FO.Formula.code x1)) -> Eq.{1} FO.Formula x0 x1)))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

2 direct dependencies 4 direct dependents

Evidence

kernel-FO.Formula.code_injective

Kind: kernel-term
Status: checked

Supports: FO.Formula.code_injective is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. It is a double recursion -- an outer FO.Formula.rec at the motive 'forall q, code p = code q -> p = q', with an inner FO.Formula.rec case analysis on q -- so the recursors' arities fix 9 x 9 = 81 cases and a skipped case is not possible.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_code_inventory -- FO.Formula.code_injective --exact --require-axiom-free

Evidence notes

Declared in crates/axeyum-lean-kernel/src/fo_numbering.rs by declare_code_injective, the same builder that produces FO.Term.code_injective; the two differ only in the constructor table they are handed. The checker fails on absence.

statement-is-injectivity-not-congruence

Kind: kernel-term
Status: checked

Supports: The theorem's INFERRED type is rebuilt in the test module from FO.Formula.code and Eq and compared by Kernel::def_eq, with the CONVERSE ('p = q -> code p = code q', true but congruence rather than injectivity) as the negative control: the two must NOT be def_eq.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_numbering::tests::formula_code_injective_states_injectivity_not_congruence --test-threads=4

Evidence notes

Without this row the fact would rest on a rendered string nobody compared against a rebuilt term.

the-numbering-computes-and-separates-the-copy-paste-pairs

Kind: kernel-term
Status: checked

Supports: FO.Formula.code is a Definition; admission says nothing about what it computes. Five formula codes are pinned by Kernel::def_eq against hand-computed numerals -- bot |-> 0, eqf (var 0) (var 0) |-> 2, imp bot bot |-> 27, all bot |-> 35, ex bot |-> 44. The separating controls are chosen at the two places a copy-paste between cases would collapse the numbering and nothing else would notice: all versus ex (same arity, same field), and the three binary connectives against each other.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_numbering::tests::formula_code_at_small_formulas fo_numbering::tests::the_two_quantifiers_get_different_codes fo_numbering::tests::the_three_binary_connectives_get_different_codes --test-threads=4

Evidence notes

These codes are small only because the pairing is the anti-diagonal one (F:fo-code-pairing-round-trip); every numeral in this kernel is unary, so under a 2^a (2b+1) pairing 'all bot' would not normalize inside a test at all and this row could not exist.

mutation-duplicate-tag

Kind: instance-pin
Status: checked

Supports: MUTATION-VERIFIED. Two mutations were applied to a scratch copy of the lane's worktree, built, run, and restored byte-for-byte with git status verified clean. Both are recorded with their measured kill counts in docs/plan/archive/lanes/arithmetization-2026-09-05.md rather than here, so this row does not repeat a number it did not measure itself.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_code:: fo_numbering:: --test-threads=4

Evidence notes

The command above is the BASELINE the mutants were measured against; the mutants themselves are source edits and are not committed. See the lane status file for what was changed and how many tests died.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_fo_numbering_prelude, lane arithmetization (W3-7, ADR-1640)",
  "source": "authored from the roadmap item; the encoding and both proofs are written here",
  "prior_art": [
    {
      "who": "Kurt Goedel",
      "what": "arithmetization of syntax",
      "year": 1931,
      "where": "Goedel, 'Ueber formal unentscheidbare Saetze der Principia Mathematica und verwandter Systeme I', Monatshefte fuer Mathematik und Physik 38 (1931)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}