GodelTargetClassPrerequisites
plain-language theorem explainer
Bundles the five classical side-conditions Gödel I needs of a formal system: a type of formulas, consistency, c.e. axioms, enough arithmetic, and an internal provability predicate. Cited only as a documentation record when contrasting RS closure with the Gödel target class. Pure structure definition; no proof content.
Claim. A record of the standard prerequisites for Gödel's first incompleteness theorem on a target system: a formal system (as a type), consistency, computable enumerability of the axiom set, expressibility of sufficient arithmetic, and internal expressibility of the system's own provability predicate. Each logical field is an unproved proposition placeholder.
background
The module proves a classical-logic fact: no real configuration $c$ can satisfy $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$, and likewise no predicate has a fixed point under negation. That content is propositional logic, not Gödel theory.
The module doc is explicit that this file does not address Gödel I. Gödel sentences satisfy $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a syntactic biconditional that is consistent; they do not satisfy $P\leftrightarrow\neg P$. The historical GodelDissolution name was misleading; this structure is only a documentation scaffold for the standard target-class hypotheses (formal system, consistency, c.e. axioms, arithmetic strength, internal provability).
Upstream edges (canonical arithmetic, trace closure, Clifford/8-tick bridges, calibration) sit in the broader foundation graph but are not used to prove anything here: the declaration has empty proof body and no theorem content.
proof idea
No proof. The declaration is a structure (definition/abbrev style) whose fields are a Type plus four Prop placeholders. Nothing is discharged; there is no tactic script, no lemma application, and no inhabitant constructed in this declaration itself.
why it matters
Exists so the framework can name, without claiming, the classical Gödel-I target class when discussing why incompleteness does not land inside the RS forcing chain. Downstream it is only re-exported under the deprecated alias GodelRequirements and mentioned beside the deprecated complete_godel_dissolution bundle (renamed to the classical-logic-and-closure theorem in this module).
It does not close T0–T8, RCL, or constant forcing. The honest meta-level claim that Gödel I has no target inside the RS chain (T-1 through T8 and constants) is outside Lean; the module points to the separate assessment note rather than treating this record as a dissolution theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.