Arnold Beckmann
The Journal of Symbolic Logic Vol. 67, No. 1, pp. 279-296
Publication year: 2002

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definition of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S^1_2 . In particular this solves an open problem formulated by Takeuti.