Harvey Friedman's "Concrete Mathematical Incompleteness" at http://www.math.osu.edu/~friedman.8/pdf/0.Intro061311.pdf cites the Hasse Minkowski theorem saying quadratic forms over a number field are equivalent if and only if they are equivalent over every completion of the field (real, complex, or $p$-adic). He says "It would appear that using standard techniques, this can be put into" first order arithmetic. He asks whether it or some stronger theorem can be made $\Pi^0_2$ or even $\Pi^0_1$.
Is there published work on this problem?