self_halting_compl_not_re
theoremverified
The complement of the diagonal halting problem is not recursively enumerable.
Statement
theorem self_halting_compl_not_re : ¬REPred (fun c : Nat.Partrec.Code => ¬(Nat.Partrec.Code.eval c (Encodable.encode c)).Dom)
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 3
- not_re_compl_of_re_and_not_computableIf a predicate is recursively enumerable but undecidable, then its complement is not recursively enumerable (Post's theorem).
- self_halting_problem_reThe diagonal halting problem, consisting of codes c such that c halts on its own code, is recursively enumerable.
- self_halting_problem_undecidableThe diagonal halting problem is not computable.
Lean source view module on GitHub
/-- The complement of the diagonal halting problem is not recursively enumerable. -/ theorem self_halting_compl_not_re : ¬REPred (fun c : Nat.Partrec.Code => ¬(Nat.Partrec.Code.eval c (Encodable.encode c)).Dom) := not_re_compl_of_re_and_not_computable self_halting_problem_re self_halting_problem_undecidable