Razborov on Unprovability

In the old commenting system, Daniel Varga had the following comment on my post on unprovability.

I guess Alexander Razborov turned to the study of Propositional Proof Systems because he wanted to prove that "proving SAT is not in P/poly" is hard in a formal sense. What is his opinion about undecidability? (Of course I know I should ask him, but he doesn't have such a nice message board. :))

I passed the question to Razborov and here is his response.

Dear Daniel, First, I understand that "undecidability" in your question should read "unprovability" (or, otherwise, I misunderstood it). And the answer to it very much depends on the strength of the formal theory we are interested in. For classical theories like Peano Arithmetic or Set Theory I do not have enough intuition (not even to mention evidence) to articulate any opinion. The only thing which seems quite sure to me is that such an independence result, if true, would not be much easier to prove than the original P vs. NP question itself... If we, however, descend in the logical hierarchy to weaker theories capturing poly-time computations (commonly known as Bounded Arithmetic), the answer becomes quite different. I do conjecture that "SAT is not in P/poly" is independent from these theories. Moreover, I believe that if we allow ourselves a standard cryptographic assumption (FACTORING is hard, for definiteness) this question might be more attainable with currently known techniques than those discussed above. Further, I expect that if we ever manage to prove such an independence result, its proof would be very illuminating in approaching the question "what's next and what are we missing?" (cf. Natural Proofs). Finally, let me mention that the introduction to the paper "Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution" (available from my Web site) contains an expanded version of some of these views. Alexander.