English
Let C be a set of Code objects (codes for partial computable functions). If membership in C is invariant under evaluation (i.e., cf and cg with equal evaluation have the same membership), then the predicate 'c ∈ C' is decidable only if C is empty or the universe.
Русский
Пусть C — множество кодов частично вычислимых функций. Если принадлежность к C инвариантна по отношению к эквалентности вычисления, то предикат 'c ∈ C' будет вычислимым только в случае, что C пусто или всеобщо.
LaTeX
$$$$\forall C \subseteq \mathrm{Code},\; (\forall cf\; cg,\; \operatorname{eval} cf = \operatorname{eval} cg \Rightarrow (cf \in C \Leftrightarrow cg \in C)) \\rightarrow \left( \mathrm{ComputablePred}(\lambda c. c \in C) \leftrightarrow (C = \emptyset \lor C = \mathrm{Set.univ})\right).$$$$
Lean4
theorem rice₂ (C : Set Code) (H : ∀ cf cg, eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)) :
(ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ := by
classical
exact
have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f => ⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
⟨fun h =>
or_iff_not_imp_left.2 fun C0 =>
Set.eq_univ_of_forall fun cg =>
let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
(hC _).2 <|
rice (eval '' C) (h.of_eq hC) (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
(Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
fun h => by { obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using Computable.const _
}⟩
