Abstract
This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and boundeddepth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system.
We define a new class of bounded arithmetic theories n^epsilonioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1),O(n^epsilon)), uniform classes of subexponentialsize boundeddepth circuits DepthSize(O(1),2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0theorems in our theories translate to subexponentialsize boundeddepth Frege proofs.
We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential boundeddepth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomialsize Frege proofs can be simulated by subexponentialsize boundeddepth Frege proofs.
Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment
NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon))
for all epsilon > 0.
BibTeX  Entry
@InProceedings{ghasemloo_et_al:LIPIcs:2013:4204,
author = {Kaveh Ghasemloo and Stephen A. Cook},
title = {{Theories for Subexponentialsize Boundeddepth Frege Proofs}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {296315},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897606},
ISSN = {18688969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4204},
URN = {urn:nbn:de:0030drops42044},
doi = {10.4230/LIPIcs.CSL.2013.296},
annote = {Keywords: Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1Frege, AC0 Frege}
}
Keywords: 

Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1Frege, AC0 Frege 
Collection: 

Computer Science Logic 2013 (CSL 2013) 
Issue Date: 

2013 
Date of publication: 

02.09.2013 