Let $X$ be a smooth projective geometrically connected variety over $\mathbb{Q}$. It is said to have good reduction at a prime $p$ is there is a smooth projective $\mathcal{X}\to \mathrm{Spec}\:\mathbb{Z}_{(p)}$ with $\mathcal{X}_{\mathbb{Q}}\approx X$.

If I understand correctly, to say that $X$ has good reduction at $p$ is naively a $\Sigma^0_2$-statement. Gro-Tsen's answer shows it can in fact be decided with a Halting oracle for ordinary Turing machines. Can it be decided with an ordinary Turing machine?