Open induction in a bounded arithmetic for TC⁰

الأصل · EN

The elementary arithmetic operations +,·,≤ on integers are well-known to be computable in the weak complexity class TC⁰, and it is a basic question what properties of these operations can be proved using only TC⁰-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC⁰. We will show that the theory VTC⁰ extended with an axiom postulating the totality of iterated multiplication (which is computable in TC⁰) proves induction for quantifier-free formulas in the language +,·,≤ (IOpen), and more generally, minimization for Σᵇ₀ formulas in the language of Buss's S₂.