# Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP

In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short proof.

But what exactly is the restriction imposed on problems/theorems? Do they have to be describable in $\Pi_1$ to use Levin's universal search?

If so, can the question like Navier-Stokes existence and smoothness problem be statble in $\Pi_1$?

• The only thing that matters is that the given proof system (in this case, ZFC or similar) has polynomial-time recognizable proofs. The complexity of the statement being proved is irrelevant. – Emil Jeřábek Jun 7 '15 at 11:17
• If downvoting, please also consider suggesting how you think the question could be improved. – usul Jun 8 '15 at 18:30
• @usul, I think the first part is answered by Emil's comment (I feel it was clear in the original post). The second part about logical complexity of stating a mathematical statement seems more suitable for Mathematics or MathOverflow. – Kaveh Jun 10 '15 at 6:15