Proving Consistency of Equational Theories in Bounded Arithmetic

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S1 2 . In particular this solves an open problem formulated by Takeuti (c.f. [5, p.5 problem 9.])

• Type: Journal
• Year: 2002
• Where: JSYML
• Authors: Arnold Beckmann
• Keywords: Equational Theories, Function Symbols, JSYML 2002, Recursive Definitions