We investigate the unprovability of NP $\not\subseteq$ P/poly in various fragments of arithmetic. The unprovability is usually obtained by showing hardness of propositional formulas encoding superpolynomial circuit lower bounds.
Firstly, we discuss few relevant techniques and known theorems. Namely, natural proofs, feasible interpolation, KPT theorem, iterability, gadget generators etc.
Then we prove some original results. We show the unprovability of superpolynomial circuit lower bounds for systems admitting certain forms of feasible interpolation (modulo a hardness assumption) and for systems roughly described as tree-like Frege systems working with formulas using only a small fraction of variables of the statement that is supposed to be proved.
These results are obtained by proving the hardness of the Nisan-Wigderson generators in corresponding proof systems.
Introduction 1
1. Bounded Arithmetic and Propositional proof systems 3
1.1 Propositional proof systems 3
1.2 Feasible provability 4
1.3 Ajtai's method 6
2. Proof complexity generators 7
3. General strategy and known techniques 8
3.1 Natural proofs 8
3.2 Feasible interpolation 9
3.3 KPT theorem 10
3.4 Formulas hard for all proof systems 11
3.5 Iterability 12
3.6 Gadget generators 12
3.7 The best known hardness result for circuit lower bounds 13
4. Nisan-Wigderson generators 15
4.1 Previous results 16
4.2 NW-generators in proof systems with EIP 17
4.3 NW-generators in strongly-sound local systems 20
5. NW-generators in strong proof systems 23
5.1 Interactive communication and KPT theorem 24
5.2 Collection schema 26
Conclusions 27
References 29
Number of pages: 36