IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Gödel Incompleteness Theorems — Structural Reference
   6
   7Two incompleteness theorems plus three related limitative results
   8(= configDim D = 5):
   9  Gödel's first incompleteness, second incompleteness,
  10  Tarski's undefinability of truth, Church's undecidability of
  11  entscheidungsproblem, Turing's halting problem.
  12
  13Each establishes a distinct limit on formal systems.
  14
  15Lean status: 0 sorry, 0 axiom.
  16-/
  17
  18namespace IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS
  19
  20inductive LimitativeResult where
  21  | godelFirst
  22  | godelSecond
  23  | tarskiUndefinability
  24  | churchUndecidability
  25  | turingHalting
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem limitativeResult_count :
  29    Fintype.card LimitativeResult = 5 := by decide
  30
  31structure GodelTheoremsCert where
  32  five_results : Fintype.card LimitativeResult = 5
  33
  34def godelTheoremsCert : GodelTheoremsCert where
  35  five_results := limitativeResult_count
  36
  37end IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS
  38