halting_problem_not_re — Mathlib

English

For every n, the predicate not REPred on halting (not halting) is not recursively enumerable; halting problem is not RE.

Русский

Для каждого n, не перечислимость предиката, описывающего останова; проблема останова не перечислима.

LaTeX

$$$$\forall n, \neg \mathrm{REPred}(\lambda c. \text{halts}(c,n)).$$$$

Lean4

theorem halting_problem_not_re (n) : ¬REPred fun c => ¬(eval c n).Dom
  | h => halting_problem _ <| computable_iff_re_compl_re'.2 ⟨halting_problem_re _, h⟩

Похожие утверждения