Abstrakt
We prove that T-Nc(1), 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 n(4kc) where k }= 1, c }= 2 unless each function f is an element of SIZE(n(k)) can be approximated by formulas {Fn}(n=1)(infinity) of subexponential size 2(O(n1/c)) with subexponential advantage: P-x is an element of{0,1)(n) [F-n(x) = f(x)] }= 1/2+1/2(O)(n(1/c)). Unconditionally, V cannot prove that for sufficiently large n, SAT does not have circuits of size n(logn).
The proof is based on an interpretation of Krajicek's proof (Krajicek, 2011 [15]) that certain NW-generators are hard for T-PV, the true universal theory in the language containing names for all p-time algorithms. (C) 2014 Elsevier B.V. All rights reserved.