Computability of arithmetical hierarchy level

Question

Is there an algorithm which for a formula P of PA outputs $\Sigma_m^0/\Pi_m^0$ such that the output is the level P belongs to in Arithmetical hierarchy? If that's not computable is there an algorithm which outputs an upper bound on the level?

Answer 1

Getting an upper bound is pretty easy: just put the formula into prenex normal form and count the quantifier types and alternations. This is something a computer can do.

... Of course, the answer this gives will sometimes be silly. For example, $$\forall x\exists y\forall z\exists w\forall u(0=1)$$ "is" $\Pi^0_5$, but we shouldn't think of it that way. So what's really being calculated is in some sense the "trivial" level of the arithmetical hierarchy that a formula lies in - what we get by simply performing basic logical operations and nothing else.

This is the best we can do, in a precise sense. Say that the optimal level of a formula $\varphi$, which I'll call "$ol(\varphi)$," is the least $n$ such that $\varphi$ is equivalent to a $\Sigma^0_n$ formula or to a $\Pi^0_n$ formula. Then it's not hard to show that the map $$\varphi\mapsto ol(\varphi)$$ is not computable - we can't computably tell whether a given $\Sigma^0_2$ sentence is equivalent to a $\Sigma^0_1$ sentence, for example.

(Here by "equivalent" I could mean either "provably equivalent over PA" or "equivalent in the structure $\mathbb{N}$" - in either case, the point is the same.)