English
If f is Turing reducible to the constant-zero oracle (the function sending every input to 0), then f is partial recursive.
Русский
Если f сводима к константному нулю орACLE, то f частично рекурсивна.
LaTeX
$$$ \forall {f : \mathbb{N} \to^. \mathbb{N}}, (f \le_T (\lambda _ . \text{Part.some } 0)) \rightarrow \text{Nat.Partrec } f $$$
Lean4
/-- If a function is recursive in the constant zero function,
then it is partial recursive.
-/
theorem partrec_of_zero (fRecInZero : f ≤ᵀ fun _ => Part.some 0) : Nat.Partrec f := by
induction fRecInZero with
repeat { constructor
}
| oracle _ hg => rw [Set.mem_singleton_iff] at hg; rw [hg]; exact Nat.Partrec.zero
| pair
| comp
| prec
| rfind =>
repeat { constructor; assumption; try assumption
}
