We prove the claim by structural induction for primitive recursive functions. A formula is bounded when every quantifier is a bounded quantifier; this is a Delta-0 formula. The graphs of the initial functions have quantifier-free definitions:
Suppose and the graphs of have existential bounded definitions. Introduce variables for the intermediate values and conjoin the graph formulasPulling all unrestricted existential witnesses to the front leaves a bounded matrix, so the required form is preserved by composition.
For primitive recursion, use Gödel beta-function sequence coding. The relationis bounded in the language of ordered rings. Given any finite sequence , choose larger than all its entries and divisible by . The moduli are pairwise coprime, so the Chinese remainder theorem supplies with for every .
Supposeand the induction hypothesis gives existential bounded graph formulas for and . Then exactly when there are coding values , together with a common witness bound , such that:Write each using , bound the variables representing by , and bound every witness used by the graph formulas for and by . All quantifiers checking the displayed finite recursion are then bounded; only and the finitely many outer coding witnesses are unrestricted existential variables. Conversely, any code passing these bounded checks satisfies the recursion equations, and induction on forces its th entry to be . This proves the existential bounded representation of a primitive recursive function.
Articles by others on the same topic
There are currently no matching articles.