34 found
Sort by:
  1. Jan Krajíček (2013). A Saturation Property of Structures Obtained by Forcing with a Compact Family of Random Variables. Archive for Mathematical Logic 52 (1-2):19-28.
    A method for constructing Boolean-valued models of some fragments of arithmetic was developed in Krajíček (Forcing with Random Variables and Proof Complexity, London Mathematical Society Lecture Notes Series, Cambridge University Press, Cambridge, 2011), with the intended applications in bounded arithmetic and proof complexity. Such a model is formed by a family of random variables defined on a pseudo-finite sample space. We show that under a fairly natural condition on the family [called compactness in Krajíček (Forcing with Random Variables and Proof (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Jan Krajíček (2011). A Note on Propositional Proof Complexity of Some Ramsey-Type Statements. Archive for Mathematical Logic 50 (1-2):245-255.
    A Ramsey statement denoted ${n \longrightarrow (k)^2_2}$ says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into a valid DNF formula RAM(n, k) of size O(n k ) and with terms of size ${\left(\begin{smallmatrix}k\\2\end{smallmatrix}\right)}$ . Let r k be the minimal n for which the statement holds. We prove that RAM(r k , k) requires exponential size constant depth Frege systems, answering a problem (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Jan Krajíček (2011). On the Proof Complexity of the Nisan–Wigderson Generator Based on a Hard Np ∩ Conp Function. Journal of Mathematical Logic 11 (01):11-27.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  4. Jan Krajíček (2010). A Form of Feasible Interpolation for Constant Depth Frege Systems. Journal of Symbolic Logic 75 (2):774-784.
    Let L be a first-order language and Φ and ψ two $\Sigma _{1}^{1}$ L-sentences that cannot be satisfied simultaneously in any finite L-structure. Then obviously the following principle Chain L,Φ,ψ (n,m) holds: For any chain of finite L-structures C 1 ,...,C m with the universe [n] one of the following conditions must fail: 1. $C_{1}\vDash \Phi $ , 2. C i ≅ C i+1 , for i = 1,...,m — 1, 3. $C_{m}\vDash \Psi $ . For each fixed L and (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  5. Jan Krajíček (2008). An Exponential Lower Bound for a Constraint Propagation Proof System Based on Ordered Binary Decision Diagrams. Journal of Symbolic Logic 73 (1):227-237.
    We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation. We define a proof system combining resolution and the OBDD proof system.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Stephen Cook & Jan Krajíček (2007). Consequences of the Provability of NP ⊆ P/Poly. Journal of Symbolic Logic 72 (4):1353 - 1371.
    We prove the following results: (i) PV proves NP ⊆ P/poly iff PV proves coNP ⊆ NP/O(1). (ii) If PV proves NP ⊆ P/poly then PV proves that the Polynomial Hierarchy collapses to the Boolean Hierarchy. (iii) $S_{2}^{1}$ proves NP ⊆ P/poly iff $S_{2}^{1}$ proves coNP ⊆ NP/O(log n). (iv) If $S_{2}^{1}$ proves NP ⊆ P/poly then $S_{2}^{1}$ proves that the Polynomial Hierarchy collapses to PNP[log n]. (v) If $S_{2}^{2}$ proves NP ⊆ P/poly then $S_{2}^{2}$ proves that the Polynomial Hierarchy (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  7. Jan Krajíček, Alan Skelley & Neil Thapen (2007). NP Search Problems in Low Fragments of Bounded Arithmetic. 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)  
     
    My bibliography  
     
    Export citation  
  8. Jan Krajíček (2005). Structured Pigeonhole Principle, Search Problems and Hard Tautologies. Journal of Symbolic Logic 70 (2):619 - 630.
    We consider exponentially large finite relational structures (with the universe {0.1}ⁿ) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that: 1. If there exists a P/poly map g: {0.1} → {0.1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  9. Jan Krajíček (2005). Hardness Assumptions in the Foundations of Theoretical Computer Science. Archive for Mathematical Logic 44 (6):667-675.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Jan Krajíček (2004). Implicit Proofs. Journal of Symbolic Logic 69 (2):387 - 397.
    We describe a general method how to construct from a propositional 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 $V_{2}^{1}$ and hence, in particular, polynomially simulates the quantified propositional calculus G and the $\pi_{1}^{b}-consequences$ of $S_{2}^{1}$ proved with one use of exponentiation. Furthermore, the soundness of iEF is not (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  11. Jan Krajíček (2004). Approximate Euler Characteristic, Dimension, and Weak Pigeonhole Principles. Journal of Symbolic Logic 69 (1):201 - 214.
    We define the notion of approximate Euler characteristic of definable sets of a first order structure. We show that a structure admits a non-trivial approximate Euler characteristic if it satisfies weak pigeonhole principle $WPHP_{n}^{2n}$ : two disjoint copies of a non-empty definable set A cannot be definably embedded into A, and principle CC of comparing cardinalities: for any two definable sets A. B either A definably embeds in B or vice versa. Also, a structure admitting a non-trivial approximate Euler characteristic (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  12. Jan Krajíček (2004). Combinatorics of First Order Structures and Propositional Proof Systems. Archive for Mathematical Logic 43 (4):427-441.
    We define the notion of a combinatorics of a first order structure, and a relation of covering between first order structures and propositional proof systems. Namely, a first order structure M combinatorially satisfies an L-sentence Φ iff Φ holds in all L-structures definable in M. The combinatorics Comb(M) of M is the set of all sentences combinatorially satisfied in M. Structure M covers a propositional proof system P iff M combinatorially satisfies all Φ for which the associated sequence of propositional (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  13. Jan Krajíček (2004). Dual Weak Pigeonhole Principle, Pseudo-Surjective Functions, and Provability of Circuit Lower Bounds. Journal of Symbolic Logic 69 (1):265 - 286.
    This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF, cf. [14, 15]. The particular tautologies we study, the τ-formulas, are obtained from any ᵊ/poly map g; they express that a string is outside of the range of g. Maps g considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the τ-formulas for at least EF from some general, plausible computational hardness hypothesis. In (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  14. Russell Impagliazzo & Jan Krajíček (2002). A Note on Conservativity Relations Among Bounded Arithmetic Theories. Mathematical Logic Quarterly 48 (3):375-377.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  15. Jan Krajicek (2001). Tautologies From Pseudo-Random Generators. Bulletin of Symbolic Logic 7 (2):197-212.
    We consider tautologies formed form a pseudo-random number generator, defined in Krajicek [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 Krajicek [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture. This is accompanied by a brief explanation, aimed at non-specialists, of the relation between prepositional proof complexity and (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  16. Jan Krajíček & Thomas Scanlon (2000). Combinatorics with Definable Sets: Euler Characteristics and Grothendieck Rings. Bulletin of Symbolic Logic 6 (3):311-330.
    We recall the notions of weak and strong Euler characteristics on a first order structure and make explicit the notion of a Grothendieck ring of a structure. We define partially ordered Euler characteristic and Grothendieck ring and give a characterization of structures that have non-trivial partially ordered Grothendieck ring. We give a generalization of counting functions to locally finite structures, and use the construction to show that the Grothendieck ring of the complex numbers contains as a subring the ring of (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  17. Mario Chiari & Jan Krajíček (1999). Lifting Independence Results in Bounded Arithmetic. Archive for Mathematical Logic 38 (2):123-138.
    We investigate the problem how to lift the non - $\forall \Sigma^b_1(\alpha)$ - conservativity of $T^2_2(\alpha)$ over $S^2_2(\alpha)$ to the expected non - $\forall \Sigma^b_i(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $S^{i+1}_2(\alpha)$ , for $i > 1$ . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a $\forall \Sigma^b_1(f)$ -consequence of $T_2(f)$ to yield the non-conservation result. Further we prove that Ramsey's theorem, a $\forall \Sigma^b_1(\alpha)$ - formula, is not provable (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  18. Matthias Baaz, Petr Hájek, David Švejda & Jan Krajíček (1998). Embedding Logics Into Product Logic. Studia Logica 61 (1):35-47.
    We construct a faithful interpretation of ukasiewicz's logic in product logic (both propositional and predicate). Using known facts it follows that the product predicate logic is not recursively axiomatizable.We prove a completeness theorem for product logic extended by a unary connective of Baaz [1]. We show that Gödel's logic is a sublogic of this extended product logic.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  19. Mario Chiari & Jan Krajíček (1998). Witnessing Functions in Bounded Arithmetic and Search Problems. 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 that are (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  20. Jan Krajíček (1998). Discretely Ordered Modules as a First-Order Extension of the Cutting Planes Proof System. Journal of Symbolic Logic 63 (4):1582-1596.
    We define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑ i a i · x i ≥ b (x i 's variables, a i 's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP- inequalities, we prove a monotone interpolation theorem (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  21. Jan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. 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 (7 more)  
     
    My bibliography  
     
    Export citation  
  22. Jan Krajíček (1995). Bounded Arithmetic, Propositional Logic, and Complexity Theory. 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, including polynomial simulations and (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  23. Jan Krajiček (1994). Lower Bounds to the Size of Constant-Depth Propositional Proofs. Journal of Symbolic Logic 59 (1):73-86.
    LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O(n3 + d) which are refutable in LK by depth d + 1 proof of size exp(O(log2 n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets Td n (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  24. Jan Krajicek (1994). Lower Bounds to the Size of Constant-Depth Propositional Proofs. Journal of Symbolic Logic 59 (1):73 - 86.
    LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O(n3 + d) which are refutable in LK by depth d + 1 proof of size exp(O(log2 n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets Td n (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  25. Jan Krajíček, Pavel Pudlák & Gaisi Takeuti (1991). Bounded Arithmetic and the Polynomial Hierarchy. Annals of Pure and Applied Logic 52 (1-2):143-153.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Jan Krajíček (1990). Exponentiation and Second-Order Bounded Arithmetic. Annals of Pure and Applied Logic 48 (3):261-276.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  27. Jan Krajíček & Pavel Pudlák (1990). Quantified Propositional Calculi and Fragments of Bounded Arithmetic. Mathematical Logic Quarterly 36 (1):29-46.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  28. Jan Krajíček & Pavel Pudlák (1989). On the Structure of Initial Segments of Models of Arithmetic. Archive for Mathematical Logic 28 (2):91-98.
    For any countable nonstandard modelM of a sufficiently strong fragment of arithmeticT, and any nonstandard numbersa, c εM, M⊨c≦a, there is a modelK ofT which agrees withM up toa and such that inK there is a proof of contradiction inT with Gödel number $ \leqq 2^{a^c } $.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  29. Jan Krajíček & Pavel Pudlák (1989). Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations. Journal of Symbolic Logic 54 (3):1063-1079.
    We consider the problem about the length of proofs of the sentences $\operatorname{Con}_S(\underline{n})$ saying that there is no proof of contradiction in S whose length is ≤ n. We show the relation of this problem to some problems about propositional proof systems.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  30. Jan Krajíček (1988). Some Results and Problems in The Modal Set Theory MST. Mathematical Logic Quarterly 34 (2):123-134.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  31. Jan Krajíček & Pavel Pudlák (1988). The Number of Proof Lines and the Size of Proofs in First Order Logic. Archive for Mathematical Logic 27 (1):69-84.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  32. Jan Krajíček (1987). A Note on Proofs of Falsehood. Archive for Mathematical Logic 26 (1):169-176.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  33. Jan Krajíček (1987). A Possible Modal Formulation of Comprehension Scheme. Zeitschrift für Mathematische Logik Und Grundlagen der Mathematik 33 (5):461-480.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  34. Jan Krajíček (1985). Some Theorems on the Lattice of Local Interpretability Types. Zeitschrift für Mathematische Logik Und Grundlagen der Mathematik 31 (29-30):449-460.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation