Open induction in a bounded arithmetic for TC^0

DOI10.1007/S00153-014-0414-7MaRDI QIDQ2339958zbMATH OpenOpenAlexFDO

Authors Emil Jeřábek

Publication date 14 April 2015

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.7435

zbMATH Keywords

bounded arithmeticthreshold circuitsvalued fieldsopen inductionreal-closed fields

Mathematics Subject Classification ID

Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Valued fields (12J10)

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,leangle$ (IOpen), and more generally, minimization for $Sigm{a}_0^b$ formulas in the language of Buss's $S_2$.

Recommendations

• Iterated multiplication in \(VTC^0\)
• On \(\text{TC}^0,\text{AC}^0\), and arithmetic circuits
• Theories for TC0 and Other Small Complexity Classes
• Publication:4893147
• On a Theory for AC0 and the Strength of the Induction Scheme

Cites work

• scientific article; zbMATH DE number 3702663 (Why is no real title available?)
• scientific article; zbMATH DE number 517079 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 1420845 (Why is no real title available?)
• scientific article; zbMATH DE number 3214534 (Why is no real title available?)
• scientific article; zbMATH DE number 3300584 (Why is no real title available?)
• Algorithms in real algebraic geometry
• Circuits in bounded arithmetic. I
• Constant Depth Reducibility
• Decomposition Problems for Modules Over Valuation Domains
• Division in logspace-uniform NC
• Efficient threshold circuits for power series
• Expressibility and Parallel Complexity
• Independence results for variants of sharply bounded induction
• Log Depth Circuits for Division and Related Problems
• Logarithmic Depth Circuits for Algebraic Functions
• Logical foundations of proof complexity
• Notes on polynomially bounded arithmetic
• On Threshold Circuits and Polynomial Computation
• On theories of bounded arithmetic for \(\mathrm{NC}^1\)
• On uniformity within \(NC^ 1\)
• Parallel computation with threshold functions
• Root finding with threshold circuits
• The strength of sharply bounded induction
• The strength of sharply bounded induction requires MSP
• Theories for TC0 and Other Small Complexity Classes
• Threshold circuits of bounded depth
• Uniform constant-depth threshold circuits for division and iterated multiplication.
• Valued Fields

Cited in

(5)

• Theories for TC0 and Other Small Complexity Classes
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Iterated multiplication in \(VTC^0\)
• Models of VTC0$\mathsf {VTC^0}$ as exponential integer parts
• Elementary analytic functions in \(\mathsf{VT}\mathsf{C}^0\)

This page was built for publication: Open induction in a bounded arithmetic for \(\mathrm{TC}^{0}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2339958)