Computability theory and the halting problem

A universal partial recursive function, Rice's theorem, and the halting problem.

References

• Mario Carneiro, Formalizing computability theory via partial recursive functions

theorem ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun (c : Nat.Partrec.Code) => c.eval ∈ C) {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

Rice's Theorem

theorem ComputablePred.rice₂ (C : Set Nat.Partrec.Code) (H : ∀ (cf cg : Nat.Partrec.Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)) : (ComputablePred fun (c : Nat.Partrec.Code) => c ∈ C) ↔ C = ∅ ∨ C = Set.univ

theorem ComputablePred.halting_problem_re (n : ℕ) : REPred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

The Halting problem is recursively enumerable

theorem ComputablePred.halting_problem (n : ℕ) : ¬ComputablePred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

The Halting problem is not computable

theorem ComputablePred.halting_problem_not_re (n : ℕ) : ¬REPred fun (c : Nat.Partrec.Code) => ¬(c.eval n).Dom