English
A predicate p is computable iff both p and its negation ¬p are recursively enumerable.
Русский
predикат p вычислим тогда и только тогда, когда p и его дополнение ¬p являются перечислимами.
LaTeX
$$$$\mathrm{ComputablePred}(p) \iff \mathrm{REPred}(p) \land \mathrm{REPred}(\neg p).$$$$
Lean4
theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a :=
⟨fun h => ⟨h.to_re, h.not.to_re⟩, fun ⟨h₁, h₂⟩ =>
⟨‹_›,
by
obtain ⟨k, pk, hk⟩ :=
Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
(by
intro a x hx y hy
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
exists_const] at hx hy
cases hy.1 hx.1)
refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_
rw [hk]
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true, true_eq_decide_iff,
and_self, exists_const, false_eq_decide_iff]
apply Decidable.em⟩⟩
