On the Difficulty of Writing Out formal Proofs in Arithmetic
Ryo Kashima, Takeshi Yamaguchi · Mathematical logic quarterly · 1997
Abstract Let ℸ be the set of Gödel numbers Gn(f) of function symbols f such that PRA ⊢ and let γ be the function such that We prove: (1) The r. e. set ℸ is m‐complete; (2) the function γ is not primitive recursive in any class of functions {f1, f2, ⃛} so long as each fi has a recursive upper bound. This implies that γ is not primitive recursive in ℸ although it is recursive in ℸ.