scholarly journals Polynomial size proofs of the propositional pigeonhole principle

1987 ◽  
Vol 52 (4) ◽  
pp. 916-927 ◽  
Author(s):  
Samuel R. Buss
Keyword(s):  
Bounded Arithmetic ◽  
Pigeonhole Principle ◽  
Polynomial Size ◽  
Frege Systems

AbstractCook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

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.

scholarly journals Proof Complexity of Modal Resolution

2021 ◽  
Author(s):  
Sarah Sigley ◽  
Olaf Beyersdorff
Keyword(s):  
Artificial Intelligence ◽  
Automated Reasoning ◽  
Proof Complexity ◽  
Pigeonhole Principle ◽  
Analytic Tableaux ◽  
Frege Systems ◽  
International Joint ◽  
Resolution Proofs ◽  
Exponential Size ◽  
Sixth International

AbstractWe investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

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.

scholarly journals Approximate counting by hashing in bounded arithmetic

2009 ◽  
Vol 74 (3) ◽  
pp. 829-860 ◽  
Author(s):  
Emil Jeřábek
Keyword(s):  
Polynomial Time ◽  
Hash Functions ◽  
Bounded Arithmetic ◽  
Pigeonhole Principle ◽  
Approximate Counting ◽  
Arithmetic Hierarchy ◽  
Relationship Of ◽  
Polynomial Time Hierarchy

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

Implicit proofs

2004 ◽  
Vol 69 (2) ◽  
pp. 387-397 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Proof System ◽  
Bounded Arithmetic ◽  
Polynomial Size ◽  
Arithmetic Theory ◽  
General Method

Abstract.We describe a general method how to construct from a prepositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described “implicitly” by polynomial size circuits.As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic theory and hence, in particular, polynomially simulates the quantified prepositional calculus G and the -consequences of proved with one use of exponentiation. Furthermore, the soundness of iEF is not provable in . An iteration of the construction yields a proof system corresponding to T2 + Exp and, in principle, to much stronger theories.

scholarly journals Uniform, Integral, and Feasible Proofs for the Determinant Identities

2021 ◽  
Vol 68 (2) ◽  
pp. 1-80
Author(s):  
Iddo Tzameret ◽  
Stephen A. Cook
Keyword(s):  
Linear Algebra ◽  
Order Theory ◽  
Bounded Arithmetic ◽  
First Order ◽  
First Order Theory ◽  
Polynomial Size ◽  
Arithmetic Theory ◽  
Integral Version ◽  
Determinant Function ◽  
Basic Determinant

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF (2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC 2 ; the latter is a first-order theory corresponding to the complexity class NC 2 consisting of problems solvable by uniform families of polynomial-size circuits and O (log 2 n )-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC 2 -circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field).

Tautologies from Pseudo-Random Generators

2001 ◽  
Vol 7 (2) ◽  
pp. 197-212 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Random Number ◽  
Random Number Generator ◽  
Bounded Arithmetic ◽  
Number Generator ◽  
Pseudo Random Number ◽  
Frege Systems ◽  
Random Generators ◽  
Pseudo Random Number Generator

AbstractWe consider tautologies formed from a pseudo-random number generator, defined in Krajíček [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajíček [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture.

Forcing on bounded arithmetic II

1998 ◽  
Vol 63 (3) ◽  
pp. 860-868 ◽  
Author(s):  
Gaisi Takeuti ◽  
Masahiro Yasumoto
Keyword(s):  
Boolean Algebra ◽  
Polynomial Time ◽  
Bounded Arithmetic ◽  
Pigeon Hole Principle ◽  
Polynomial Size ◽  
Np Complete ◽  
Computable Functions

Forcing method on Bounded Arithmetic was first introduced by J. B. Paris and A. Wilkie in [10]. Then in [1], [2] and [3], M. Ajtai used the method to get excellent results on the pigeon hole principle and the modulo p counting principle. The forcing method on Bounded arithmetic was further developed by P. Beame, J. Krajíček and S. Riis in [4], [7], [6], [8], [5], [12], [11], [13]. It should be noted that J. Krajíček and P. Pudlák used an idea of Boolean valued in [9] and also Boolean valued notion is efficiently used for model theoretic constructions in [7], [6], [8], [5].In our previous paper [14], we developed a Boolean valued version of forcing on Bounded Arithmetic using Boolean algebra which is generated by polynomial size circuits from Boolean variables and discussed its relation with NP = co-NP problem and P = NP problem. Especially we proved the following theorem and related theorems as Theorems 2, 3 and 4 in Section 2.Theorem. If M[G] is not a model of S2, then NP ≠ co-NP and therefore P ≠ NP.However in the proof of the Theorem, we used a consequence of P = NP. More precisely we used the following as a consequence of NP = co-NP, though it is a consequence of P = NP but not a consequence of NP = co-NP.Suppose that NP = co-NP holds. Then there exists an NP-complete predicate ∃x ≤ t(a) A(x,a) with sharply bounded A(x, a) and a sharply bounded B(y, a) such that ∃x ≤ t(a) A(x,a) ↔ ∀y ≤ s(a)B(y, a). Then there exists polynomial time computable functions f and g such that the following two sequents hold.

scholarly journals Approximate counting in bounded arithmetic

2007 ◽  
Vol 72 (3) ◽  
pp. 959-993 ◽  
Author(s):  
Emil Jeřábek
Keyword(s):  
Complexity Classes ◽  
Bounded Arithmetic ◽  
Boolean Circuits ◽  
Pigeonhole Principle ◽  
Approximate Counting

AbstractWe 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 PV1 + dWPHP(PV).

Sign in / Sign up

Export Citation Format

Share Document