Circuit lower bounds in bounded arithmetics

We prove that TNC1, the true universal first-order theory in the language containing names for all uniform NC1 algorithms, cannot prove that for sufficiently large n, SAT is not computable by circuits of size n4kc where k≥1,c≥2 unless each function f∈SIZE(nk) can be approximated by formulas {Fn}n=1∞ of subexponential size 2O(n1/c) with subexponential advantage: Px∈{0,1}n[Fn(x)=f(x)]≥1/2+1/2O(n1/c). Unconditionally, V0 cannot prove that for sufficiently large n, SAT does not have circuits of size nlog⁡n. The proof is based on an interpretation of Krajíček's proof (Krajíček, 2011 [15]) that certain NW-generators are hard for TPV, the true universal theory in the language containing names for all p-time algorithms.