TC ^0的有界算术中的开归纳
Open induction in a bounded arithmetic for TC^0
摘要：
众所周知，整数上的初等算术运算$+,\cdot,\le$在弱复杂性类$\mathrm{TC}^0$中是可计算的，并且这些运算的什么性质可以仅使用$\mathrm{TC}^0$ -可计算对象来证明是一个基本问题，即，有界算术理论中的一个对应于$\mathrm{TC}^0$。我们将证明，理论$\mathit{VTC}^0$扩展与公理假设的总体迭代乘法（这是可计算的$\mathrm{TC}^0$）证明归纳的量词免费公式的语言$\langle +,\cdot,\le \rangle$（IOpen），更一般地说，最小化$Σ^b_0$公式的语言巴斯的$S_2$。
英文摘要：
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 $Σ^b_0$ formulas in the language of Buss's $S_2$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
