Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem
type: Item
instance of: scholarly article
title: Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem
zbMATH Open document ID: 1251.03077
author: Neil Thapen
published in: Archive for Mathematical Logic
publication date: 2011-11-23T00:00:00Z
review text: In the paper a new characterization of the strict \(\forall \Sigma^{b}_{j}\)-sentences provable using \(\Sigma^{b}_{k}\)-induction for \(1 \leq j \leq k\) is given. As an application it is shown that in a certain sense Buss's witnessing theorem for strict \(\Sigma^{b}_{k}\)-formulas already holds over the relatively weak theory PV. A combinatorial principle is exhibited with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth-\(j\) Frege refutations form a strict hierarchy with \(j\), and hence that the relativized bounded arithmetic hierarchy can be separated by a family of \(\forall \Sigma^{b}_{1}\)-sentences.
reviewed by: Roman Murawski
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68Q15
zbMATH DE Number: 5977557
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: proof complexity
zbMATH Keywords: search problems
MaRDI profile type: Publication
full work available at URL: s00153-011-0240-0
OpenAlex ID: W1979972097
cites work: POLYNOMIAL LOCAL SEARCH IN THE POLYNOMIAL HIERARCHY AND WITNESSING IN FRAGMENTS OF BOUNDED ARITHMETIC
cites work: Q3081638
cites work: Q3794177
cites work: Polynomial size proofs of the propositional pigeonhole principle
cites work: Q3476809
cites work: Relating the bounded arithmetic and polynomial time hierarchies
cites work: An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
cites work: Witnessing functions in bounded arithmetic and search problems
cites work: Lifting independence results in bounded arithmetic
cites work: Q4133141
cites work: What are the \(\forall \Sigma_ 1^ b\)-consequences of \(T_ 2^ 1\) and \(T_ 2^ 2\)?
cites work: Herbrandizing search problems in Bounded Arithmetic
cites work: Q4856172
cites work: A form of feasible interpolation for constant depth Frege systems
cites work: Quantified propositional calculi and fragments of bounded arithmetic
cites work: Bounded arithmetic and the polynomial hierarchy
cites work: An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
cites work: NP search problems in low fragments of bounded arithmetic
cites work: On induction-free provability
cites work: Q3689182
cites work: Exponential lower bounds for the pigeonhole principle
cites work: Q5477362
cites work: Fragments of bounded arithmetic and the lengths of proofs
cites work: The provably total search problems of bounded arithmetic
cites work: Notes on polynomially bounded arithmetic
DOI: 10.1007/S00153-011-0240-0
Recommended article: The provably total search problems of bounded arithmetic
Recommended article: Q4266170
Recommended article: Bounded arithmetic, proof complexity and two papers of Parikh
Recommended article: Q4357061
Recommended article: Q3081638
Recommended article: Herbrandizing search problems in Bounded Arithmetic
Recommended article: Q4856172
Recommended article: Total search problems in bounded arithmetic and improved witnessing
Recommended article: Q4850554
Recommended article: Q2753676
description: scientific article; zbMATH DE number 5977557