Strong co-nondeterministic lower bounds for NP cannot be proved feasibly

We show unconditionally that Cook's theory PV 1 formalizing poly-time reasoning cannot prove, for any non-deterministic poly-time machine M defining a language L(M ), that L(M ) is inapproximable by co-nondeterministic circuits of sub-exponential size. In fact, our unprovability result holds also for a theory which supports a fragment of Jeřábek's theory of approximate counting APC 1 . We also show similar unconditional unprovability results for the conjecture of Rudich about the existence of super-bits.