Results for 'bounded arithmetic'

996 found
Order:
  1.  7
    Herbrandizing Search Problems in Bounded Arithmetic.Jiří Hanika - 2004 - Mathematical Logic Quarterly 50 (6):577-586.
    We study search problems and reducibilities between them with known or potential relevance to bounded arithmetic theories. Our primary objective is to understand the sets of low complexity consequences of theories Si2 and Ti2 for a small i, ideally in a rather strong sense of characterization; or, at least, in the standard sense of axiomatization. We also strive for maximum combinatorial simplicity of the characterizations and axiomatizations, eventually sufficient to prove conjectured separation results. To this end two techniques (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  2. Approximate Counting by Hashing in Bounded Arithmetic.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (3):829-860.
    We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3. On Interpretations of Bounded Arithmetic and Bounded Set Theory.Richard Pettigrew - 2009 - Notre Dame Journal of Formal Logic 50 (2):141-152.
    In 'On interpretations of arithmetic and set theory', Kaye and Wong proved the following result, which they considered to belong to the folklore of mathematical logic.

    THEOREM 1 The first-order theories of Peano arithmetic and Zermelo-Fraenkel set theory with the axiom of infinity negated are bi-interpretable.

    In this note, I describe a theory of sets that is bi-interpretable with the theory of bounded arithmetic IDelta0 + exp. Because of the weakness of this theory of sets, I cannot straightforwardly (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  4.  46
    Higher Complexity Search Problems for Bounded Arithmetic and a Formalized No-Gap Theorem.Neil Thapen - 2011 - Archive for Mathematical Logic 50 (7-8):665-680.
    We give a new characterization of the strict $\forall {\Sigma^b_j}$ sentences provable using ${\Sigma^b_k}$ induction, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss’s witnessing theorem for strict ${\Sigma^b_k}$ formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  5.  6
    A Remark on Independence Results for Sharply Bounded Arithmetic.Jan Johannsen - 1998 - Mathematical Logic Quarterly 44 (4):568-570.
    The purpose of this note is to show that the independence results for sharply bounded arithmetic of Takeuti [4] and Tada and Tatsuta [3] can be obtained and, in case of the latter, improved by the model-theoretic method developed by the author in [2].
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  15
    An Unexpected Separation Result in Linearly Bounded Arithmetic.Arnold Beckmann & Jan Johannsen - 2005 - Mathematical Logic Quarterly 51 (2):191-200.
    The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  7.  9
    An Independence Result on Weak Second Order Bounded Arithmetic.Satoru Kuroda - 2001 - Mathematical Logic Quarterly 47 (2):183-186.
    We show that length initial submodels of S12 can be extended to a model of weak second order arithmetic. As a corollary we show that the theory of length induction for polynomially bounded second order existential formulae cannot define the function division.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8.  16
    A Note on Conservativity Relations Among Bounded Arithmetic Theories.Russell Impagliazzo & Jan Krajíček - 2002 - Mathematical Logic Quarterly 48 (3):375-377.
    For all i ≥ 1, Ti+11 is not ∀Σb2-conservative over Ti1.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  9.  10
    On the Provability Logic of Bounded Arithmetic.Rineke Verbrugge & Alessandro Berarducci - 1991 - Annals of Pure and Applied Logic 61 (1-2):75-93.
    Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  10.  23
    A Note on the E1 Collection Scheme and Fragments of Bounded Arithmetic.Zofia Adamowicz & Leszek Aleksander Kołodziejczyk - 2010 - Mathematical Logic Quarterly 56 (2):126-130.
    We show that for each n ≥ 1, if T2n does not prove the weak pigeonhole principle for Σbn functions, then the collection scheme B Σ1 is not finitely axiomatizable over T2n. The same result holds with Sn2 in place of T 2n.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  11.  12
    Separations of First and Second Order Theories in Bounded Arithmetic.Masahiro Yasumoto - 2005 - Archive for Mathematical Logic 44 (6):685-688.
  12.  10
    A Counterexample to Polynomially Bounded Realizability of Basic Arithmetic.Mohammad Ardeshir, Erfan Khaniki & Mohsen Shahriari - 2019 - Notre Dame Journal of Formal Logic 60 (3):481-489.
    We give a counterexample to the claim that every provably total function of Basic Arithmetic is a polynomially bounded primitive recursive function.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13.  15
    Strict $${\Pi^1_1}$$ -Reflection in Bounded Arithmetic.António M. Fernandes - 2010 - Archive for Mathematical Logic 49 (1):17-34.
    We prove two conservation results involving a generalization of the principle of strict ${\Pi^1_1}$ -reflection, in the context of bounded arithmetic. In this context a separation between the concepts of bounded set and binary sequence seems to emerge as fundamental.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  44
    Notes on Polynomially Bounded Arithmetic.Domenico Zambella - 1996 - Journal of Symbolic Logic 61 (3):942-966.
    We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   30 citations  
  15.  25
    Bounded Arithmetic, Propositional Logic, and Complexity Theory.Jan Krajíček - 1995 - Cambridge University Press.
    This book presents an up-to-date, unified treatment of research in bounded arithmetic and complexity of propositional logic, with emphasis on independence proofs and lower bound proofs. The author discusses the deep connections between logic and complexity theory and lists a number of intriguing open problems. An introduction to the basics of logic and complexity theory is followed by discussion of important results in propositional proof systems and systems of bounded arithmetic. More advanced topics are then treated, (...)
    Direct download  
     
    Export citation  
     
    Bookmark   13 citations  
  16.  14
    Structure and Definability in General Bounded Arithmetic Theories.Chris Pollett - 1999 - Annals of Pure and Applied Logic 100 (1-3):189-245.
    The bounded arithmetic theories R2i, S2i, and T2i are closely connected with complexity theory. This paper is motivated by the questions: what are the Σi+1b-definable multifunctions of R2i? and when is one theory conservative over another? To answer these questions we consider theories , and where induction is restricted to prenex formulas. We also define which has induction up to the 0 or 1-ary L2-terms in the set τ. We show and and for . We show that the (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  17.  6
    Relating the Bounded Arithmetic and Polynomial Time Hierarchies.Samuel R. Buss - 1995 - Annals of Pure and Applied Logic 75 (1-2):67-77.
    The bounded arithmetic theory S2 is finitely axiomatized if and only if the polynomial hierarchy provably collapses. If T2i equals S2i + 1 then T2i is equal to S2 and proves that the polynomial time hierarchy collapses to ∑i + 3p, and, in fact, to the Boolean hierarchy over ∑i + 2p and to ∑i + 1p/poly.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  18. Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
    A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  19.  23
    NP Search Problems in Low Fragments of Bounded Arithmetic.Jan Krajíček, Alan Skelley & Neil Thapen - 2007 - Journal of Symbolic Logic 72 (2):649 - 672.
    We give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories $T_{2}^{2}$ and $T_{3}^{2}$.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  20. Approximate Counting in Bounded Arithmetic.Emil Jeřábek - 2007 - Journal of Symbolic Logic 72 (3):959 - 993.
    We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV₁ + dWPHP(PV).
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  21.  28
    Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic.Arnold Beckmann & Samuel R. Buss - 2009 - Journal of Mathematical Logic 9 (1):103-138.
    The complexity class of [Formula: see text]-polynomial local search 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, (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  22.  12
    Bounded Arithmetic for NC, ALogTIME, L and NL.P. Clote & G. Takeuti - 1992 - Annals of Pure and Applied Logic 56 (1-3):73-117.
    We define theories of bounded arithmetic, whose definable functions and relations are exactly those in certain complexity classes. Based on a recursion-theoretic characterization of NC in Clote , the first-order theory TNC, whose principal axiom scheme is a form of short induction on notation for nondeterministic polynomial-time computable relations, has the property that those functions having nondeterministic polynomial-time graph Θ such that TNC x y Θ are exactly the functions in NC, computable on a parallel random-access machine in (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  23.  9
    The Provably Total NP Search Problems of Weak Second Order Bounded Arithmetic.Leszek Aleksander Kołodziejczyk, Phuong Nguyen & Neil Thapen - 2011 - Annals of Pure and Applied Logic 162 (6):419-446.
    We define a new NP search problem, the “local improvement” principle, about labellings of an acyclic, bounded-degree graph. We show that, provably in , it characterizes the consequences of and that natural restrictions of it characterize the consequences of and of the bounded arithmetic hierarchy. We also show that over V0 it characterizes the consequences of V1 and hence that, in some sense, a miniaturized version of the principle gives a new characterization of the consequences of . (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  24.  14
    Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.Samuel R. Buss & Aleksandar Ignjatović - 1995 - Annals of Pure and Applied Logic 74 (3):221-244.
    Samuel R. Buss and Aleksandar Ignjatović. Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  25.  45
    Witnessing Functions in Bounded Arithmetic and Search Problems.Mario Chiari & Jan Krajíček - 1998 - Journal of Symbolic Logic 63 (3):1095-1115.
    We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in 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 are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  26.  7
    Structures Interpretable in Models of Bounded Arithmetic.Neil Thapen - 2005 - Annals of Pure and Applied Logic 136 (3):247-266.
    We look for a converse to a result from [N. Thapen, A model-theoretic characterization of the weak pigeonhole principle, Annals of Pure and Applied Logic 118 175–195] that if the weak pigeonhole principle fails in a model K of bounded arithmetic, then there is an end-extension of K interpretable inside K. We show that if a model J of an induction-free theory of arithmetic is interpretable inside K, then either J is isomorphic to an initial segment of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  27.  5
    A Bounded Arithmetic AID for Frege Systems.Toshiyasu Arai - 2000 - Annals of Pure and Applied Logic 103 (1-3):155-199.
    In this paper we introduce a system AID of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss’ propositional consistency proof of Frege systems F in Buss 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  28.  18
    On the Herbrand Notion of Consistency for Finitely Axiomatizable Fragments of Bounded Arithmetic Theories.Leszek Aleksander Kołodziejczyk - 2006 - Journal of Symbolic Logic 71 (2):624 - 638.
    Modifying the methods of Z. Adamowicz's paper Herbrand consistency and bounded arithmetic [3] we show that there exists a number n such that ⋃m Sm (the union of the bounded arithmetic theories Sm) does not prove the Herbrand consistency of the finitely axiomatizable theory $S_{3}^{n}$.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  29.  50
    A Small Reflection Principle for Bounded Arithmetic.Rineke Verbrugge & Albert Visser - 1994 - Journal of Symbolic Logic 59 (3):785-812.
    We investigate the theory IΔ 0 + Ω 1 and strengthen [Bu86. Theorem 8.6] to the following: if NP ≠ co-NP. then Σ-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  30.  12
    A Note on Sharply Bounded Arithmetic.Jan Johannsen - 1994 - Archive for Mathematical Logic 33 (2):159-165.
    We prove some independence results for the bounded arithmetic theoryR 2 0 , and we define a class of functions that is shown to be an upper bound for the class of functions definable by a certain restricted class of ∑ 1 b in extensions ofR 2 0.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  31.  7
    Ordinal Notations and Well-Orderings in Bounded Arithmetic.Arnold Beckmann, Chris Pollett & Samuel R. Buss - 2003 - Annals of Pure and Applied Logic 120 (1-3):197-223.
    This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  32.  7
    Ordinal Notations and Well-Orderings in Bounded Arithmetic (Vol 120, Pg 197, 2003).Arnold Beckmann, Samuel R. Buss & Chris Pollett - 2003 - Annals of Pure and Applied Logic 123 (1-3):291-291.
    This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  4
    Preservation Theorems and Restricted Consistency Statements in Bounded Arithmetic.Arnold Beckmann - 2004 - Annals of Pure and Applied Logic 126 (1-3):255-280.
    We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  34.  10
    Generalized Quantifier and a Bounded Arithmetic Theory for LOGCFL.Satoru Kuroda - 2007 - Archive for Mathematical Logic 46 (5-6):489-516.
    We define a theory of two-sort bounded arithmetic whose provably total functions are exactly those in ${\mathcal{F}_{LOGCFL}}$ by way of a generalized quantifier that expresses computations of SAC 1 circuits. The proof depends on Kolokolova’s conditions for the connection between the provable capture in two-sort theories and descriptive complexity.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  35.  8
    Upper and Lower Ramsey Bounds in Bounded Arithmetic.Kerry Ojakian - 2005 - Annals of Pure and Applied Logic 135 (1-3):135-150.
    Pudlák shows that bounded arithmetic proves an upper bound on the Ramsey number Rr . We will strengthen this result by improving the bound. We also investigate lower bounds, obtaining a non-constructive lower bound for the special case of 2 colors , by formalizing a use of the probabilistic method. A constructive lower bound is worked out for the case when the monochromatic set size is fixed to 3 . The constructive lower bound is used to prove two (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  36.  6
    Polynomial Induction and Length Minimization in Intuitionistic Bounded Arithmetic.Morteza Moniri - 2005 - Mathematical Logic Quarterly 51 (1):73-76.
    It is shown that the feasibly constructive arithmetic theory IPV does not prove LMIN, unless the polynomial hierarchy CPV-provably collapses. It is proved that PV plus LMIN intuitionistically proves PIND. It is observed that PV + PIND does not intuitionistically prove NPB, a scheme which states that the extended Frege systems are not polynomially bounded.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37.  11
    On Theories of Bounded Arithmetic for NC 1.Emil Jeřábek - 2011 - Annals of Pure and Applied Logic 162 (4):322-340.
    We develop an arithmetical theory and its variant , corresponding to “slightly nonuniform” . Our theories sit between and , and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of -formulas provable in admit L-uniform polynomial-size Frege proofs.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  38.  24
    A Sorting Network in Bounded Arithmetic.Emil Jeřábek - 2011 - Annals of Pure and Applied Logic 162 (4):341-355.
    We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory , under the assumption of the existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  39.  8
    Exponentiation and Second-Order Bounded Arithmetic.Jan Krajíček - 1990 - Annals of Pure and Applied Logic 48 (3):261-276.
    V i 2 ⊢A iff for some term t :S i 2 ⊢ “2 i exists→ A”, a bounded first-order formula, i ≥1. V i 2 is not Π b 1 -conservative over S i 2 . Any model of V 2 not satisfying Exp satisfies the collection scheme BΣ 0 1 . V 1 3 is not Π b 1 -conservative over S 2.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  40.  10
    End Extensions of Models of Linearly Bounded Arithmetic.Domenico Zambella - 1997 - Annals of Pure and Applied Logic 88 (2-3):263-277.
    We show that every model of IΔ0 has an end extension to a model of a theory where log-space computable function are formalizable. We also show the existence of an isomorphism between models of IΔ0 and models of linear arithmetic LA.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  41.  23
    Proving Consistency of Equational Theories in Bounded Arithmetic.Arnold Beckmann† - 2002 - Journal of Symbolic Logic 67 (1):279-296.
    We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  42.  9
    On Bounded Arithmetic Augmented by the Ability to Count Certain Sets of Primes.Alan R. Woods & Ch Cornaros - 2009 - Journal of Symbolic Logic 74 (2):455-473.
    Over 25 years ago, the first author conjectured in [15] that the existence of arbitrarily large primes is provable from the axioms I Δ₀(π) + def(π), where π(x) is the number of primes not exceeding x, IΔ₀(π) denotes the theory of Δ₀ induction for the language of arithmetic including the new function symbol π, and de f(π) is an axiom expressing the usual recursive definition of π. We prove a modified version in which π is replaced by a more (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  43.  15
    On the Scheme of Induction for Bounded Arithmetic Formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (3):261-302.
  44.  15
    Bounded Arithmetic and the Polynomial Hierarchy.Jan Krajíček, Pavel Pudlák & Gaisi Takeuti - 1991 - Annals of Pure and Applied Logic 52 (1-2):143-153.
    T i 2 = S i +1 2 implies ∑ p i +1 ⊆ Δ p i +1 ⧸poly. S 2 and IΔ 0 ƒ are not finitely axiomatizable. The main tool is a Herbrand-type witnessing theorem for ∃∀∃ П b i -formulas provable in T i 2 where the witnessing functions are □ p i +1.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   34 citations  
  45.  21
    Jan Krajíček, Pavel Pudlák, and Gaisi Takeuti. Bounded Arithmetic and the Polynomial Hierarchy. Ibid., Vol. 52 , Pp. 143–153. - Samuel R. Buss. Relating the Bounded Arithmetic and Polynomial Time Hierarchies. Ibid., Vol. 75 , Pp. 67–77. - Domenico Zambella. Notes on Polynomially Bounded Arithmetic. The Journal of Symbolic Logic, Vol. 61 , Pp. 942–966. [REVIEW]Stephen Cook - 1999 - Journal of Symbolic Logic 64 (4):1821-1823.
  46. Alternating Minima and Maxima, Nash Equilibria and Bounded Arithmetic.Pavel Pudlák & Neil Thapen - 2012 - Annals of Pure and Applied Logic 163 (5):604-614.
  47.  14
    Quantified Propositional Calculi and Fragments of Bounded Arithmetic.Jan Krajíček & Pavel Pudlák - 1990 - Mathematical Logic Quarterly 36 (1):29-46.
  48.  23
    Quantified Propositional Calculi and Fragments of Bounded Arithmetic.Jan Krajíček & Pavel Pudlák - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):29-46.
  49.  29
    Consistency Proof of a Fragment of Pv with Substitution in Bounded Arithmetic.Yoriyuki Yamagata - 2018 - Journal of Symbolic Logic 83 (3):1063-1090.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  50.  14
    Mitsuru Tada and Makoto Tatsuta. The Function ⌊a/M⌋ in Sharply Bounded Arithmetic. Archive for Mathematical Logic, Vol. 37 No. 1 , Pp. 51–57. [REVIEW]Fernando Ferreira - 2001 - Bulletin of Symbolic Logic 7 (3):391.
1 — 50 / 996