| Popis: |
A weak formal theory of arithmetic is developed, entirely analogous to classical arithmetic but with two separate kinds of variables: induction variables and quantifier variables. The point is that the provably recursive functions are now more feasibly computable than in the classical case, lying between Grzegorczyk’s E2 and E3, and their computational complexity can be characterized in terms of the logical complexity of their termination proofs. Previous results of Leivant are reworked and extended in this new setting, with quite different proof theoretic methods. |
