English
Let C be a set of functions from N to N. If the membership predicate 'eval c ∈ C' is computable, then either C is empty or C is the set of all such functions; in particular, no nontrivial property of computable functions is decidable.
Русский
Пусть C — множество функций ℕ→ℕ. Если предикат принадлежности 'eval c ∈ C' вычислим, то либо C пусто, либо C состоит из всех таких функций; следовательно, нет нетривиированного свойства вычислимых функций, которое было бы решаемо.
LaTeX
$$$\forall C \subseteq \mathrm{PFun}(\mathbb{N},\mathbb{N}),\; \mathrm{REPred}(\lambda c. \operatorname{eval} c \in C) \Rightarrow (C = \emptyset \lor C = \mathrm{Set.univ}).$$$
Lean4
/-- **Rice's Theorem** -/
theorem rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => eval c ∈ C) {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g)
(fC : f ∈ C) : g ∈ C := by
obtain ⟨_, h⟩ := h
obtain ⟨c, e⟩ :=
fixed_point₂
(Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂ ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂
simp only [Bool.cond_decide] at e
by_cases H : eval c ∈ C
· simp only [H, if_true] at e
change (fun b => g b) ∈ C
rwa [← e]
· simp only [H, if_false] at e
rw [e] at H
contradiction
