Parent, T.: Universal Primitive Recursion
We first offer a minimal version of PRA where the subscript on any function symbol f_i allows us to recover the axiom defining the function symbol. An algorithm is then constructed where the relevant subscript guides the generation of a "canonical proof" of f_i(i,n) = m. (Halting occurs when a line is reached with zero occurrences of 'f' to the right of '='.) The resulting algorithm is then shown to satisfy all standard criteria for being p.r. This suggests that the standard diagonal objection d
Tags
