Open induction in a bounded arithmetic for TC^0

TL;DR

This paper demonstrates that a bounded arithmetic theory corresponding to the complexity class TC^0 can prove induction and minimization principles for elementary arithmetic operations, linking computational complexity with formal proof systems.

Contribution

It shows that extending the theory VTC^0 with iterated multiplication allows proving induction for quantifier-free formulas within TC^0, connecting computational and proof-theoretic properties.

Findings

Proves IOpen in VTC^0 with iterated multiplication

Establishes minimization for Σ^b_0 formulas in S_2

Links TC^0 computability with formal induction principles

Abstract

The elementary arithmetic operations $+,\cdot,\le$ on integers are well-known to be computable in the weak complexity class $\mathrm{TC}^0$, and it is a basic question what properties of these operations can be proved using only $\mathrm{TC}^0$-computable objects, i.e., in a theory of bounded arithmetic corresponding to $\mathrm{TC}^0$. We will show that the theory $\mathit{VTC}^0$ extended with an axiom postulating the totality of iterated multiplication (which is computable in $\mathrm{TC}^0$) proves induction for quantifier-free formulas in the language $\langle +,\cdot,\le \rangle$ (IOpen), and more generally, minimization for $\Sigma^b_0$ formulas in the language of Buss's $S_2$.