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.
Read more about this topic: Craig's Theorem
Famous quotes containing the word primitive:
“The lumberers rarely trouble themselves to put out their fires, such is the dampness of the primitive forest; and this is one cause, no doubt, of the frequent fires in Maine, of which we hear so much on smoky days in Massachusetts.”
—Henry David Thoreau (1817–1862)