Premium
On the Difficulty of Writing Out formal Proofs in Arithmetic
Author(s) -
Kashima Ryo,
Yamaguchi Takeshi
Publication year - 1997
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19970430305
Subject(s) - primitive recursive function , mathematics , mathematical proof , set (abstract data type) , function (biology) , μ operator , class (philosophy) , recursive functions , arithmetic , discrete mathematics , combinatorics , computer science , geometry , evolutionary biology , artificial intelligence , biology , programming language
Let ℸ be the set of Gödel numbers Gn( f ) of function symbols f such that PRA ⊢ and let γ be the function such that\documentclass{article}\pagestyle{empty}\begin{document}$$\begin{array}{*{20}c} {\gamma (n) = \left\{ {\mathop G\limits_0 n({\rm PRA} - {\rm proof}\,{\rm of}\,\forall x(f(x) = 0))} \right.} & {\mathop {{\rm if}\,n = }\limits_{otherwise.} Gn(f) \in \Gamma,}\\\end{array} $$\end{document} We prove: (1) The r. e. set ℸ is m‐complete; (2) the function γ is not primitive recursive in any class of functions { f 1 , f 2 , ⃛} so long as each f i has a recursive upper bound. This implies that γ is not primitive recursive in ℸ although it is recursive in ℸ.