Undecidability of Membership for RE Languages

This file proves that membership cannot be decided for recursively enumerable (RE) languages in general. More precisely, there exists an RE predicate whose membership is not computable.

The proof uses the classical halting-problem undecidability result from Mathlib:

• ComputablePred.halting_problem_re — the halting predicate is RE.
• ComputablePred.halting_problem — the halting predicate is not computable.

Together these immediately yield: there exists an RE predicate that is not computable, which is the formal content of the statement "membership is undecidable for RE languages."

Main results

• RE_membership_undecidable — there exists a recursively enumerable predicate that is not computably decidable.
• RE_membership_undecidable' — the halting predicate (for input 0) is RE but not computably decidable.

theorem RE_membership_undecidable' : (REPred fun (c : Nat.Partrec.Code) => (c.eval 0).Dom) ∧ ¬ComputablePred fun (c : Nat.Partrec.Code) => (c.eval 0).Dom

The halting predicate (for input 0) is RE but not computably decidable.

theorem RE_membership_undecidable : ∃ (p : Nat.Partrec.Code → Prop), REPred p ∧ ¬ComputablePred p

There exists a recursively enumerable predicate that is not computably decidable.

This is the formal statement of the classical result that "membership is undecidable for RE languages": while RE languages/predicates are those for which membership can be confirmed (semi-decided) by a Turing machine, there is no algorithm that can decide membership (i.e., always halt with a yes/no answer) for every RE language.

theorem recursivelyEnumerable_computableMembership_undecidable {RE : Set (Language Unit)} : ¬ComputableMembership RE partrecCodeDomainLanguageOf

Membership for RE codes is not uniformly computable.