Jan Krajíček, Pavel Pudlák, and Gaisi Takeuti. Bounded arithmetic and the polynomial hierarchy. Ibid., vol. 52 (1991), pp. 143–153. - Samuel R. Buss. Relating the bounded arithmetic and polynomial time hierarchies. Ibid., vol. 75 (1995), pp. 67–77. - Domenico Zambella. Notes on polynomially bounded arithmetic. The journal of symbolic logic, vol. 61 (1996), pp. 942–966.

1999 ◽  
Vol 64 (4) ◽  
pp. 1821-1823
Author(s):  
Stephen Cook
Keyword(s):  
Polynomial Time ◽  
Polynomial Hierarchy ◽  
Symbolic Logic ◽  
Bounded Arithmetic

Gödel sentences of bounded arithmetic

2000 ◽  
Vol 65 (3) ◽  
pp. 1338-1346 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Polynomial Time ◽  
Special Kind ◽  
Interesting Case ◽  
Polynomial Hierarchy ◽  
Bounded Arithmetic ◽  
Original Language ◽  
Close Relationship ◽  
Np Problem ◽  
Good Contrast ◽  
Computable Functions

In [1], S. Buss introduced the systems of Bounded Arithmetic for (i = 0,1,2,…) which has a close relationship to classes in polynomial hierarchy.In [4], we defined a very special kind of proof-predicate Prfi for which gives detailed information on bounds of free variables used in the proof. There we also introduced infinitely many Gödel sentences for Prfi (k = 0, 1, 2, …) and showed that the properties of Prfi and are closely related to the P ≠ NP problem. Then we presented many conjectures on Prfi and which imply P ≠ NP.Now in [2], Feferman emphasized that the arithmetization of metamathematics must be carried out intensionally. Bounded Arithmetic is a very interesting case in this sense.In this paper, we also introduce the usual proof-predicate PRFi for and infinitely many Gödel sentences for PRFi(k= 0, 1, 2, …). Then we show that (Prfi, )and (PRFi, ) form a good contrast, this contrast is also closely related to the P ≠ NP problem, and present more conjectures which imply P ≠ NP.As in [4] we define to be the following extension of Buss' original .(1) We add finitely many function symbols which express polynomial time computable functions to Buss' original language of .(2) All basic axioms on function symbols and ≤ can be expressed by initial sequents without logical symbols.

scholarly journals POLYNOMIAL LOCAL SEARCH IN THE POLYNOMIAL HIERARCHY AND WITNESSING IN FRAGMENTS OF BOUNDED ARITHMETIC

2009 ◽  
Vol 09 (01) ◽  
pp. 103-138 ◽  
Author(s):  
ARNOLD BECKMANN ◽  
SAMUEL R. BUSS
Keyword(s):  
Local Search ◽  
Polynomial Time ◽  
Complexity Class ◽  
Polynomial Hierarchy ◽  
Bounded Arithmetic ◽  
Weak Base ◽  
Base Theory ◽  
Definable Functions ◽  
New Formula

The complexity class of [Formula: see text]-polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the [Formula: see text]-definable functions of [Formula: see text] are characterized in terms of [Formula: see text]-PLS problems. These [Formula: see text]-PLS problems can be defined in a weak base theory such as [Formula: see text], and proved to be total in [Formula: see text]. Furthermore, the [Formula: see text]-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new [Formula: see text]-principle that is conjectured to separate [Formula: see text] and [Formula: see text].

scholarly journals FRAGMENTS OF APPROXIMATE COUNTING

2014 ◽  
Vol 79 (2) ◽  
pp. 496-525 ◽  
Author(s):  
SAMUEL R. BUSS ◽  
LESZEK ALEKSANDER KOŁODZIEJCZYK ◽  
NEIL THAPEN
Keyword(s):  
Polynomial Time ◽  
Open Problem ◽  
Bounded Arithmetic ◽  
Pigeonhole Principle ◽  
Approximate Counting ◽  
Image Position

AbstractWe study the long-standing open problem of giving $\forall {\rm{\Sigma }}_1^b$ separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the $\forall {\rm{\Sigma }}_1^b$ Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNP functions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of $T_2^1$ augmented with the surjective weak pigeonhole principle for polynomial time functions.

A second order version of S2i and U21

1991 ◽  
Vol 56 (3) ◽  
pp. 1038-1063 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Second Order ◽  
The Other ◽  
Polynomial Hierarchy ◽  
Bounded Arithmetic ◽  
Conservative Extension ◽  
First Order ◽  
Second Order Systems ◽  
Separation Problems

In [1] S. Buss introduced systems of bounded arithmetic , , , (i = 1, 2, 3, …). and are first order systems and and are second order systems. and are closely related to and respectively in the polynomial hierarchy, and and are closely related to PSPACE and EXPTIME respectively. One of the most important problems in bounded arithmetic is whether the hierarchy of bounded arithmetic collapses, i.e. whether = or = for some i, or whether = , or whether is a conservative extension of S2 = ⋃i. These problems are relevant to the problems whether the polynomial hierarchy PH collapses or whether PSPACE = PH or whether PSPACE = EXPTIME. It was shown in [4] that = implies and consequently the collapse of the polynomial hierarchy. We believe that the separation problems of bounded arithmetic and the separation problems of computational complexities are essentially the same problem, and the solution of one of them will lead to the solution of the other.

scholarly journals Bounded arithmetic and the polynomial hierarchy

1991 ◽  
Vol 52 (1-2) ◽  
pp. 143-153 ◽  
Author(s):  
Jan Krajíček ◽  
Pavel Pudlák ◽  
Gaisi Takeuti
Keyword(s):  
Polynomial Hierarchy ◽  
Bounded Arithmetic

Witnessing functions in bounded arithmetic and search problems

1998 ◽  
Vol 63 (3) ◽  
pp. 1095-1115 ◽  
Author(s):  
Mario Chiari ◽  
Jan Krajíček
Keyword(s):  
Partial Order ◽  
Polynomial Time ◽  
Bounded Arithmetic ◽  
Pigeonhole Principle ◽  
Search Problems ◽  
Strict Partial Order ◽  
Conservation Result ◽  
Time Structures

AbstractWe investigate the possibility to characterize (multi)functions that are-definable with smalli(i= 1, 2, 3) in fragments of bounded arithmeticT2in terms of natural search problems defined over polynomial-time structures. We obtain the following results:(1) A reformulation of known characterizations of (multi)functions that areand-definable in the theoriesand.(2) New characterizations of (multi)functions that areand-definable in the theory.(3) A new non-conservation result: the theoryis not-conservative over the theory.To prove that the theoryis not-conservative over the theory, we present two examples of a-principle separating the two theories:(a) the weak pigeonhole principle WPHP(a2,f, g) formalizing that no functionfis a bijection betweena2andawith the inverseg,(b) the iteration principle Iter(a, R, f) formalizing that no functionfdefined on a strict partial order ({0,…, a},R) can have increasing iterates.

Delineating classes of computational complexity via second order theories with weak set existence principles. I

1995 ◽  
Vol 60 (1) ◽  
pp. 103-121 ◽  
Author(s):  
Aleksandar Ignjatović
Keyword(s):  
Computational Complexity ◽  
Polynomial Time ◽  
Second Order ◽  
Complexity Classes ◽  
Bounded Arithmetic ◽  
Recursive Functions ◽  
Speed Up ◽  
Bounded Complexity ◽  
Polynomial Time Hierarchy ◽  
Comprehension Axiom

AbstractIn this paper we characterize the well-known computational complexity classes of the polynomial time hierarchy as classes of provably recursive functions (with graphs of suitable bounded complexity) of some second order theories with weak comprehension axiom schemas but without any induction schemas (Theorem 6). We also find a natural relationship between our theories and the theories of bounded arithmetic (Lemmas 4 and 5). Our proofs use a technique which enables us to “speed up” induction without increasing the bounded complexity of the induction formulas. This technique is also used to obtain an interpretability result for the theories of bounded arithmetic (Theorem 4).

Sign in / Sign up

Export Citation Format

Share Document