English

Open induction in a bounded arithmetic for TC^0

Logic in Computer Science 2015-03-25 v2 Logic

Abstract

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

Keywords

Cite

@article{arxiv.1404.7435,
  title  = {Open induction in a bounded arithmetic for TC^0},
  author = {Emil Jeřábek},
  journal= {arXiv preprint arXiv:1404.7435},
  year   = {2015}
}

Comments

35 pages

R2 v1 2026-06-22T04:02:04.814Z