not_re_compl_of_re_and_not_computable
theoremverified
If a predicate is recursively enumerable but undecidable, then its complement is not recursively enumerable (Post's theorem).
Statement
theorem not_re_compl_of_re_and_not_computable {α : Type*} [Primcodable α] {p : α → Prop} (hre : REPred p) (hnc : ¬ComputablePred p) : ¬REPred (fun a => ¬p a)
- 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 complement of an undecidable recursively enumerable predicate is not recursively enumerable. -/ theorem not_re_compl_of_re_and_not_computable {α : Type*} [Primcodable α] {p : α → Prop} (hre : REPred p) (hnc : ¬ComputablePred p) : ¬REPred (fun a => ¬p a) := fun hrec => hnc (ComputablePred.computable_iff_re_compl_re'.2 ⟨hre, hrec⟩)