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 n2kc where k1c4 unless each function fSIZE(nk) can be approximated by formulas Fnn=1 of subexponential size 2O(n2c) with subexponenital advantage: Px01n[Fn(x)=f(x)]12+12O(n2c). Unconditionally, V0 cannot prove that for sufficiently large n SAT does not have circuits of size nlogn. The proof is based on an interpretation of Krajicek's proof (2011) that certain NW-generators are hard for TPV, the true universal theory in the language containing names for all p-time algorithms.
展开▼
