This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to (...) produce one of A and B which is true. In addition, there is superexponential lower bound on the size of terms which fulfill the existential property of intuitionistic predicate logic. There are superexponential upper bounds for these problems, so the lower bounds are essentially optimal. (shrink)

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], and show that this analysis can be formalized in the bounded arithmetic system VNC^1 (corresponding to the “NC^1 reasoning”). As a corollary, we prove the assumption made by Jeřábek [28] that a construction of certain bipartite expander graphs can be formalized in VNC^1 . This in turn implies that every proof in Gentzen's sequent calculus LK of a (...) monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlák [9]. (shrink)

We give the first systematic study of strong isomorphism reductions, a notion of reduction more appropriate than polynomial time reduction when, for example, comparing the computational complexity of the isomorphim problem for different classes of structures. We show that the partial ordering of its degrees is quite rich. We analyze its relationship to a further type of reduction between classes of structures based on purely comparing for every n the number of nonisomorphic structures of cardinality at most n in both (...) classes. Furthermore, in a more general setting we address the question of the existence of a maximal element in the partial ordering of the degrees. (shrink)

We give a uniform proof of the theorems of Yao and Beigel–Tarui representing ACC predicates as constant depth circuits with MODm\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {MOD}_{m}$$\end{document} gates and a symmetric gate. The proof is based on a relativized, generalized form of Toda’s theorem expressed in terms of closure properties of formulas under bounded universal, existential and modular counting quantifiers. This allows the main proofs to be expressed in terms of formula classes instead of Boolean circuits. (...) The uniform version of the Beigel–Tarui theorem is then obtained automatically via the Furst–Saxe–Sipser and Paris–Wilkie translations. As a special case, we obtain a uniform version of Razborov and Smolensky’s representation of AC0[p]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {AC}^{0}[p]$$\end{document} circuits. The paper is partly expository, but is also motivated by the desire to recast Toda’s theorem, the Beigel–Tarui theorem, and their proofs into the language of bounded arithmetic. However, no knowledge of bounded arithmetic is needed. (shrink)

We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...) number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs. (shrink)

We extend results of Bonet, Buss and Pitassi on Bondy’s Theorem and of Nozaki, Arai and Arai on Bollobás’ Theorem by proving that Frankl’s Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parametert, we prove that Frankl’s Theorem has polynomial size AC0-Frege proofs from instances of the pigeonhole principle.

This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.

We introduce martingales defined by probabilistic strategies, in which randomness is used to decide whether to bet. We show that different criteria for the success of computable probabilistic strategies can be used to characterize ML-randomness, computable randomness, and partial computable randomness. Our characterization of ML-randomness partially addresses a critique of Schnorr by formulating ML randomness in terms of a computable process rather than a computably enumerable function.

We consider tautologies expressing equivalence‐chain properties in the spirit of Thapen and Krajíček, which are candidates for exponentially separating depth k and depth Frege proof systems. We formulate a special case where the initial member of the equivalence chain is fully specified and the equivalence‐chain implications are actually equivalences. This special case is shown to lead to polynomial size resolution refutations. Thus it cannot be used for separating depth k and depth propositional systems. We state some Håstad switching lemma conditions (...) that restrict the possible propositional proofs in more general situations. (shrink)