# The Hasse Minkowski theorem in Peano arithmetic

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?

• The standard methods he mentions are standard in practice. The usual proofs of Hasse-Minkowski over $\mathbb{Q}$ (the case for other number fields is similar) reduce the $p$-adic calculation for any given rational quadratic form to calculations mod $p^n$ for $n$ specifiable from the coefficients of the form. And that is the usual point of using the theorem. But has anyone gone into the specific quantifier complexity of the theorem? – Colin McLarty Aug 3 '13 at 1:20