Global regularity for Navier-Stokes on the torus is $\Pi_2^0$; this is essentially an observation of Bourgain (who made it in the more general context of supercritical equations), and which I sketched out in this paper http://arxiv.org/abs/0710.1604 . Basically, Navier-Stokes is equivalent to the assertion that for all $T, E > 0$, there exists an $M$ such that all initial data with $H^1$ norm at most $E$, there exists a solution up to time $T$ whose $H^1$ norm is always bounded by $M$. Now if such a claim is the case, it can be verified (using rigorous perturbation theory) by constructing a sufficient number of approximate solutions to a sufficient number of choices of initial data, and verifying that all of these approximate solutions have norm at most $M/2$ (say) up to time $T$, where "sufficient number" is something explicit that depends on $E, T, M$, and the nature of the approximation can be discretised at an explicit scale that also depends on $E,T,M$. So Navier-Stokes takes the form $\forall T,E \exists M: P(T,E,M)$ where $P(T,E,M)$ is something that can be verified in finite time for each $T,E,M$. (In fact, for each $E$ there is an explicit time $T = T(E)$ for which one needs to verify $P(T,E,M)$, and beyond which global regularity is easily obtained from the energy dissipation, so the claim even simplifies a little to $\forall E \exists M: P( T(E), E, M)$.)

It looks very difficult to me, however, to make Navier-Stokes $\Pi^0_1$. This would basically amount to being able to describe all possible "blowup scenarios" by a countable set, and to be able to determine whether each such blowup scenario can actually happen in finite time. While some blowup scenarios (particularly "stable", "approximately self-similar" ones) can be described and verified in such a manner, it's not clear whether all of them can.

Global regularity for Navier-Stokes on the torus is (logically equivalent to) a $\Pi_2^0$ statement; this is essentially an unpublished observation of Bourgain (who made it in the more general context of supercritical equations), which I sketched out in this paper http://arxiv.org/abs/0710.1604 . Basically, Navier-Stokes is equivalent to the assertion that for all $T, E > 0$, there exists an $M$ such that all initial data with $H^1$ norm at most $E$, there exists a solution up to time $T$ whose $H^1$ norm is always bounded by $M$. Now if such a claim is the case, it can be verified (using rigorous perturbation theory) by constructing a sufficient number of approximate solutions to a sufficient number of choices of initial data, and verifying that all of these approximate solutions have norm at most $M/2$ (say) up to time $T$, where "sufficient number" is something explicit that depends on $T, E, M$, and the nature of the approximation can be discretised at an explicit scale that also depends on $T,E,M$. So Navier-Stokes is equivalent to a statement of the form $\forall T,E \exists M: P(T,E,M)$ where $P(T,E,M)$ is something that can be verified in finite time for each $T,E,M$ (which can be taken to be rational numbers). (In fact, for each $E$ there is an explicit time $T = T(E)$ for which one needs to verify $P(T,E,M)$, and beyond which global regularity is easily obtained from the energy dissipation, so the claim even simplifies a little to $\forall E \exists M: P( T(E), E, M)$.)

It looks very difficult to me, however, to make Navier-Stokes equivalent to a $\Pi^0_1$ statement. This would basically amount to being able to describe all possible "blowup scenarios" by a countable set, and to be able to determine whether each such blowup scenario can actually happen in finite time. While some blowup scenarios (particularly "stable", "approximately self-similar" ones) can be described and verified in such a manner, it's not clear whether all of them can.

Global regularity for Navier-Stokes on the torus is $\Pi_2^0$; this is essentially an observation of Bourgain (who made it in the more general context of supercritical equations), and which I sketched out in this paper http://arxiv.org/abs/0710.1604 . Basically, Navier-Stokes is equivalent to the assertion that for all $T, E > 0$, there exists an $M$ such that all initial data with $H^1$ norm at most $E$, there exists a solution up to time $T$ whose $H^1$ norm is always bounded by $M$. Now if such a claim is the case, it can be verified (using rigorous perturbation theory) by constructing a sufficient number of approximate solutions to a sufficient number of choices of initial data, and verifying that all of these approximate solutions have norm at most $M/2$ (say) up to time $T$, where "sufficient number" is something explicit that depends on $E, T, M$, and the nature of the approximation can be discretised at an explicit scale that also depends on $E,T,M$. So Navier-Stokes takes the form $\forall T,E \exists M: P(T,E,M)$ where $P(T,E,M)$ is something that can be verified in finite time for each $T,E,M$.

It looks very difficult to me, however, to make Navier-Stokes $\Pi^0_1$. This would basically amount to being able to describe all possible "blowup scenarios" by a countable set, and to be able to determine whether each such blowup scenario can actually happen in finite time. While some blowup scenarios (particularly "stable", "approximately self-similar" ones) can be described and verified in such a manner, it's not clear whether all of them can.

Global regularity for Navier-Stokes on the torus is $\Pi_2^0$; this is essentially an observation of Bourgain (who made it in the more general context of supercritical equations), and which I sketched out in this paper http://arxiv.org/abs/0710.1604 . Basically, Navier-Stokes is equivalent to the assertion that for all $T, E > 0$, there exists an $M$ such that all initial data with $H^1$ norm at most $E$, there exists a solution up to time $T$ whose $H^1$ norm is always bounded by $M$. Now if such a claim is the case, it can be verified (using rigorous perturbation theory) by constructing a sufficient number of approximate solutions to a sufficient number of choices of initial data, and verifying that all of these approximate solutions have norm at most $M/2$ (say) up to time $T$, where "sufficient number" is something explicit that depends on $E, T, M$, and the nature of the approximation can be discretised at an explicit scale that also depends on $E,T,M$. So Navier-Stokes takes the form $\forall T,E \exists M: P(T,E,M)$ where $P(T,E,M)$ is something that can be verified in finite time for each $T,E,M$. (In fact, for each $E$ there is an explicit time $T = T(E)$ for which one needs to verify $P(T,E,M)$, and beyond which global regularity is easily obtained from the energy dissipation, so the claim even simplifies a little to $\forall E \exists M: P( T(E), E, M)$.)

It looks very difficult to me, however, to make Navier-Stokes $\Pi^0_1$. This would basically amount to being able to describe all possible "blowup scenarios" by a countable set, and to be able to determine whether each such blowup scenario can actually happen in finite time. While some blowup scenarios (particularly "stable", "approximately self-similar" ones) can be described and verified in such a manner, it's not clear whether all of them can.