We prove closure under the defining schemes for primitive recursive functions, keeping all unbounded existential variables outside a bounded arithmetic formula. A bounded quantifier means or , where does not contain . All formulas are interpreted in the standard natural numbers.
First we need a finite sequence code using only the permitted language of ordered rings. Define the bounded arithmetic formulaFor given , it specifies the unique remainder of modulo . In particular the quotient and remainder variables are bounded by arithmetic terms; division is not a new language symbol.
Every finite list can be coded by some pair . Choose larger than every list entry and divisible by every integer from to . The moduli are pairwise coprime. Indeed a prime dividing both cannot divide , but then divides ; since and is divisible by that integer, this is impossible. The Chinese remainder theorem gives with for every . Since , each holds. This is Gödel beta-function sequence coding. The external choice of a divisible proves that codes exist; factorial and exponentiation do not occur in the existential bounded representation of a primitive recursive function.
For the zero function, successor function and projections use , and . These formulas need no auxiliary variables. For function composition in recursion theory, suppose have representations with bounded arithmetic formulas . A bounded arithmetic formula for isTreat every as an auxiliary variable in the outer existential block. The logical conjunction is true for some such variables exactly when is the desired output.
Now supposeBy structural induction for primitive recursive functions, assume and are bounded arithmetic formulas representing . We code the values with . For finite witness array coding, give each component of the step witness another code pair , so that the witness at step is the remainder specified by .
With these code pairs and as free auxiliary variables, take the following bounded arithmetic formula:The displayed line breaks are only for readability: the bounded quantifiers on the last three lines bind the entire bracket. If , their empty block and logical conjunction are omitted. Expanding every occurrence of leaves only bounded quantifiers, logical conjunctions, the bounded arithmetic formulas already obtained, and the symbols .
If , take the actual finite computation values and select witnesses for the finitely many true instances of , together with witnesses for . The Gödel beta-function sequence coding provides and the finitely many . These make true. Conversely, suppose some code pairs and initial witnesses make true. The unique remainders of give values . The initial clause makes . Every step clause makes , since its coded witnesses satisfy the representing matrix for . Induction on gives , and the final remainder clause gives . This argument includes , when the step condition is empty.
Closure under the initial functions of recursion theory, composition and primitive recursion provesCoding the step witnesses is essential: leaving an unrestricted existential witness block inside would not give the required syntactic form.
Articles by others on the same topic
There are currently no matching articles.