Polylogarithmic cuts in models of V^0

DOI10.2168/LMCS-9(1:16)2013MaRDI QIDQ4913779zbMATH OpenFDO

Authors Sebastian Müller

Publication date 9 April 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

bounded arithmeticcutsmodels of bounded arithmeticproof complexitysimulations of proof systemstwo-sorted theories

Mathematics Subject Classification ID

Models of arithmetic and set theory (03C62) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Nonstandard models of arithmetic (03H15)

Abstract: We study initial cuts of models of weak two-sorted Bounded Arithmetics with respect to the strength of their theories and show that these theories are stronger than the original one. More explicitly we will see that polylogarithmic cuts of models of $mathbf{V}^0$ are models of $mathbf{VNC}^1$ by formalizing a proof of Nepomnjascij's Theorem in such cuts. This is a strengthening of a result by Paris and Wilkie. We can then exploit our result in Proof Complexity to observe that Frege proof systems can be sub exponentially simulated by bounded depth Frege proof systems. This result has recently been obtained by Filmus, Pitassi and Santhanam in a direct proof. As an interesting observation we also obtain an average case separation of Resolution from AC0-Frege by applying a recent result with Tzameret.

Recommendations

• Theories for subexponential-size bounded-depth Frege proofs
• On theories of bounded arithmetic for \(\mathrm{NC}^1\)
• Logical foundations of proof complexity
• Regular cuts in models of bounded arithmetic
• Cuts and overspill properties in models of bounded arithmetic

Cited in

(5)

• Iterated multiplication in VTC^0
• Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\)
• Collapsing modular counting in bounded arithmetic and constant depth propositional proofs
• The polynomial and linear time hierarchies in V⁰
• The Polynomial and Linear Hierarchies in V0

This page was built for publication: Polylogarithmic cuts in models of \(\mathbf{V}^{0}\)

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