self_halting_problem_re
theoremverified
The diagonal halting problem, consisting of codes c such that c halts on its own code, is recursively enumerable.
Statement
theorem self_halting_problem_re : REPred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom)
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- self_halting_compl_not_reThe complement of the diagonal halting problem is not recursively enumerable.
Lean source view module on GitHub
/-- The diagonal halting problem (self-halting problem) is recursively enumerable. -/ theorem self_halting_problem_re : REPred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom) := (Nat.Partrec.Code.eval_part.comp Computable.id Computable.encode).dom_re