<p>In <a href="https://cstheory.stackexchange.com/questions/2800/if-p-np-could-we-obtain-proofs-of-goldbachs-conjecture-etc">If P=NP, could we obtain proofs of Goldbach&#39;s Conjecture etc.?</a> 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. </p>

<p>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? </p>

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

CC BY-SA 3.0
2015-06-07T11:17:44.800Z
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
CC BY-SA 3.0
2015-06-08T18:30:13.833Z
If downvoting, please also consider suggesting how you think the question could be improved.
usul
CC BY-SA 3.0
2015-06-10T06:15:21.363Z
@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 [math.se] or [mathoverflow.se].
Kaveh
<cc.complexity-theory><proof-complexity><descriptive-complexity><automated-theorem-proving>
Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP
time
# Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP

(Asked by: username_0 on 2015-06-07)

In [If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?](https://cstheory.stackexchange.com/questions/2800/if-p-np-could-we-obtain-proofs-of-goldbachs-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$?

**Tags:** cc.complexity-theory, proof-complexity, descriptive-complexity, automated-theorem-proving
> **Comments:**
> **username_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.  
> **username_2**: If downvoting, please also consider suggesting how you think the question could be improved.  
> **username_3**: @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 [math.se] or [mathoverflow.se].  

---

## 0 answers

