LimitativeResult
This inductive definition enumerates the five classical limitative results in formal logic: Gödel's first incompleteness theorem, Gödel's second incompleteness theorem, Tarski's undefinability of truth, Church's undecidability of the Entscheidungsproblem, and Turing's halting problem. Researchers in foundations of mathematics or computability theory cite the enumeration when confirming the exact count of such results inside the Recognition Science structural setup. The definition lists the five cases explicitly and derives decidable equality, a
claimThe set of limitative results consists of five elements given by the constructors for Gödel's first incompleteness theorem, Gödel's second incompleteness theorem, Tarski's undefinability of truth, Church's undecidability of the Entscheidungsproblem, and Turing's halting problem.
background
The module supplies a structural reference to the Gödel incompleteness theorems together with three related limitative results, for a total of five items that the text equates with configDim D = 5. Each result marks a distinct boundary on what formal systems can achieve: incompleteness for consistent systems containing arithmetic, undefinability of a truth predicate, undecidability of the decision problem, and undecidability of the halting problem. The module records that the Lean development contains zero sorry statements and zero axioms.
proof idea
The declaration is an inductive definition whose body consists solely of five explicit constructors. The deriving clause automatically supplies DecidableEq, Repr, BEq, and Fintype; no tactics or lemmas are invoked.
why it matters in Recognition Science
The enumeration is the direct input to GodelTheoremsCert, whose single field records that the cardinality equals five, and to the theorem limitativeResult_count that discharges the equality by decision. It therefore supplies the structural count required by the module's claim that the five results correspond to D = 5 inside the Recognition Science framework.
scope and limits
- Does not contain proofs of any of the five results.
- Does not link the results to physical constants or the forcing chain.
- Does not address consistency strength or other meta-theoretic properties.
- Does not admit additional limitative results beyond the five constructors.
formal statement (Lean)
20inductive LimitativeResult where
21 | godelFirst
22 | godelSecond
23 | tarskiUndefinability
24 | churchUndecidability
25 | turingHalting
26 deriving DecidableEq, Repr, BEq, Fintype
27