Induction and Primitive Recursion in a Resource Conscious Logic — With a New Suggestion of How to Assign a Measure of Complexity to Primitive Recursive Functions
Uwe Petersen · 2008
In (22), I presented a general approach to the definition of primitive recursive functions on the basis of a higher order logic without contraction employing a new kind of infinitary inference, the Z-inferences. The present paper is essentially a rewriting of this approach based on fixed-point constructions for the primitive recursive functions and a par- ticular concern for the number of Z-inferences involved in proving results such as the recursion equations of primitive recursive functions and their totality.