Open induction in a bounded arithmetic for TC^0

DOI10.1007/S00153-014-0414-7zbMATH Open1371.03090arXiv1404.7435OpenAlexW2103436750MaRDI QIDQ2339958FDOQ2339958

Authors: Emil Jeřábek 

Publication date: 14 April 2015

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

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$.

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

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

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)

Cites Work

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

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)