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 4 k c where k ≥ 1 , c ≥ 2 unless each function f ∈ SIZE ( n k ) can be approximated by formulas { F n } n = 1 ∞ of subexponential size 2 O ( n 1 / c ) with subexponential advantage: P x ∈ { 0 , 1 } n [ F n ( x ) = f ( x ) ] ≥ 1 / 2 + 1 / 2 O ( n 1 / 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 (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.