Total computable diagonal over primitive recursive syntax
ID: total-computable-diagonal-over-primitive-recursive-syntax
Enumerate all valid unary primitive recursive functions in intension by their decidable codes , and interpret each extension . The function is a total computable function, since each finite construction terminates. If it were primitive recursive, some would equal , giving . Repeated extensions in the syntax enumeration do not affect this argument.
New to topics? Read the docs here!