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 by a Halting oracle for ordinary Turing machines. Can it be decided by an ordinary Turing machine?

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 by a halting oracle for ordinary Turing machines. Can it be decided by an ordinary Turing machine?

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?

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 by a Halting oracle for ordinary Turing machines. Can it be decided by an ordinary Turing machine?

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 a $\Sigma^0_2$-statement. So it can be decided by a single query to a third order halting oracle. Can we do better?

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?