2

Consider the set of terms in the language of arithmetic built from the constant 0, and the functions $'$, +, and $\cdot$. Each such term is of course equal to some numeral (i.e., term of the form $0'''^{...} $.)

Is the function that takes the Godel number of such a term into the Godel number of the numeral to which it is equal primitive recursive? (I am happy to work with any reasonable Godel numbering.)

provocateur
  • 636
  • It probably depends on the Gödel numbering, and in particular whether the height of a tree is encoded in its root. – Peter Taylor Jul 31 '19 at 05:00
  • 1
    My intuition is the opposite - as long as the coding and decoding functions are primitive recursive, there should be a way of using primitive recursion to define the value of a term. – provocateur Jul 31 '19 at 05:04
  • Ah, yes: you can use the value representing the tree as a very loose upper bound on the height. – Peter Taylor Jul 31 '19 at 05:16
  • Yes, something like that seems right. Surely someone has worked out the details, but I don't seem to be able to find anything in the usual books. – provocateur Jul 31 '19 at 05:19

0 Answers0