Goedel's first incompleteness theorem, in the hypothesis-carrying form (OPEN in this ledger)

Identifier: F:fo-first-incompleteness
Proof route: Not assigned
External status: proved
Axiom footprint: Empty

Recorded description

If a theory is consistent and REPRESENTS ITS OWN PROVABILITY -- that is, there is a formula Prov with one free variable satisfying the two derivability conditions relating Prov to actual derivability -- then the Goedel sentence built by the diagonal lemma from the negation of Prov is not derivable in it. NOT ESTABLISHED HERE, and deliberately stated in the form that takes representability as an explicit HYPOTHESIS rather than proving it: representability of provability is the part of Goedel I that is a construction over the arithmetization, and it is out of reach until the arithmetization can decode. Consistency of the calculus with an empty context IS established (F:fo-consistency), and the numbering the Goedel sentence would be built from IS established (F:fo-formula-code-injective); what is missing is the diagonal lemma (F:fo-diagonal-lemma) and, under it, the decoder (F:fo-formula-decoder).

Formal statement

theorem FO.goedel_first : ((x0 : FO.Context) -> ((x1 : FO.Formula) -> ((x2 : ((x3 : FO.Formula) -> ((x4 : FO.Provable x0 x3) -> FO.Provable x0 (FO.Formula.subst x1 (FO.Subst.cons (FO.Formula.numeral (FO.Formula.code x3)) FO.Subst.id))))) -> ((x3 : ((x4 : FO.Formula) -> ((x5 : FO.Provable x0 (FO.Formula.subst x1 (FO.Subst.cons (FO.Formula.numeral (FO.Formula.code x4)) FO.Subst.id))) -> FO.Provable x0 x4))) -> ((x4 : Not (FO.Provable x0 FO.Formula.bot)) -> ((x5 : FO.Formula) -> ((x6 : Iff (FO.Provable x0 x5) (FO.Provable x0 (FO.Formula.imp (FO.Formula.subst x1 (FO.Subst.cons (FO.Formula.numeral (FO.Formula.code x5)) FO.Subst.id)) FO.Formula.bot))) -> Not (FO.Provable x0 x5))))))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "not established in this ledger",
  "source": "this row records the target the arithmetization is aimed at, and the measured distance to it after lane arithmetization landed the numbering (W3-7, ADR-1640)",
  "prior_art": [
    {
      "who": "Kurt Goedel; J. Barkley Rosser",
      "what": "the first incompleteness theorem; Rosser removed the omega-consistency hypothesis from the second half",
      "year": 1936,
      "where": "Goedel 1931; Rosser, 'Extensions of some theorems of Goedel and Church', JSL 1 (1936)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}