We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all logics (...) of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

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.

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.

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

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

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 polylogarithmic parallel (...) time with a polynomial number of processors.0 We then define three theories of weak second-order arithmetic which respectively characterize relations in the classes of alternating logarithmic time, logspace and nondeterministic logspace. (shrink)

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

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 -CA and (...) a quantified theory QALV of an equational system ALV in Clote 57–106). Hence ALV also proves the soundness of F. (shrink)