Craig's Theorem - Primitive Recursive Axiomatizations

Primitive Recursive Axiomatizations

The proof above shows that for each recursively enumerable set of axioms there is a recursive set of axioms with the same deductive closure. A set of axioms is primitive recursive if there is a primitive recursive function that decides membership in the set. To obtain a primitive recursive aximatization, instead of replacing a formula with

one instead replaces it with

(*)

where f(x) is a function that, given i, returns a computation history showing that is in the original recursively enumerable set of axioms. It is possible for a primitive recursive function to parse an expression of form (*) to obtain and j. Then, because Kleene's T predicate is primitive recursive, it is possible for a primitive recursive function to verify that j is indeed a computation history as required.