Quadratic forms in models of \(I\Delta _{0}+\Omega _{1}\). I (Q2382276)

The paper develops a theory of binary quadratic forms over weak fragments of Peano Arithmetic. The ultimate goal (not yet fulfilled) is Gauss's proof of quadratic reciprocity. The development follows \textit{J. W. S. Cassels}'s book [Rational quadratic forms. London etc.: Academic Press (1978; Zbl 0395.10029)]. After a quick introduction to Pell and anti-Pell equations, quadratic reciprocity law, and quadratic forms, the authors discuss \(\Delta_0\)-definability of equivalence of binary quadratic forms over models of \(I\Delta_0+\Omega_1\). Let \(\mathcal M\) be a model. Then, a form \(f\) is \(\mathcal M\)-equivalent to \(g\) if there are matrices \(C\) and \(E\) over \(\mathcal M\) such that \(g(\bar v)=f(C\bar v)\) and \(f(\bar v)=g(E\bar v)\). It is shown that the relation of equivalence between two forms is not \(\Delta_0\)-definable in the language including a function symbol for \(x^{\log y}\). However, there are other positive results, for example, for positive definite forms the equivalence relation is \(\Delta_0\)-definable. The main result is the following version of Gauss's Finiteness Theorem: Let \({\mathcal M}\) be a model of \(I\Delta_0+\Omega_1\). There is a fixed polynomial \(P(x)\) with integer coefficients such that any quadratic form of determinant \(d\) is properly \({\mathcal M}\)-equivalent to a form with the same determinant but whose coefficients are all bounded by \(P(d)\). The paper concludes with a section establishing a group law on the set of equivalence classes of proper \(\mathcal M\)-equivalence.