[Proof Complexity] New preprint

[Jan Pich]

Dear colleagues,

A new preprint of mine, titled "Circuit Lower Bounds in Bounded Arithmetics"
is available at: www.karlin.mff.cuni.cz/~pich/elsarticle-template-num.pdf
Comments, corrections, and suggestions are appreciated.


Best Wishes

Jan Pich

Abstract: We prove that $T_{NC^1}$, the true universal first-order theory in the language containing names for all uniform $NC^1$ algorithms, cannot prove that for sufficiently large $n$, SAT is not computable by circuits of size $n^{2kc}$ where $k\geq 1, c\geq 4$ unless each function $f\in SIZE(n^k)$ can be approximated by formulas $\{F_n\}^{\infty}_{n=1}$ of subexponential size $2^{O(n^{2/c})}$ with subexponential advantage: $P_{x\in \{0,1\}^n}[F_n(x)=f(x)]\geq 1/2+1/2^{O(n^{2/c})}$

Unconditionally, $V^0$ cannot prove that for sufficiently large $n$ SAT does not have circuits of size $n^{\log n}$

The proof is based on an interpretation of Krajicek's proof (2011) that certain NW-generators are hard for $T_{PV}$, the true universal theory in the language containing names for all p-time algorithms.