Some new results on decidability for elementary algebra and geometry (Q714712)

From the authors' introduction: ``The purpose of this paper is to investigate decidability for more general classes of real vector spaces.'' The main issue is the decidability or undecidability of the various theories which consist of sentences in a two-sorted first-order language: one sort for vectors and one sort for real scalars. In particular, all theories of inner product spaces turn out to be decidable, while undecidability reigns in the case of normed spaces, the only exception being the theory of a 1-dimensional space. In the opening section, the authors introduce notation and terminology and then go on to consider the expressive power of the language for normed spaces vis à vis the language for inner product spaces. Theorem: There are first-order sentences that hold in all complete metric spaces (resp. Banach spaces) but not in all metric spaces (resp. normed spaces). Furthermore, the class of complete metric spaces (resp. Banach spaces) is not an axiomatizable subclass of the class of metric spaces (resp. normed spaces). For inner product spaces, the authors prove that a sentence holds in every space of dimension \(d\geq k\) iff it holds in \(\mathbb R^k\) where \(k\) is the distinct number of vector variables in the sentence. This leads to the conclusion: ``the theories of inner product spaces and Hilbert spaces with various dimensional constraints can all be decided via a simple reduction to the first-order theory of the real numbers.'' Undecidability for theories of normed spaces is achieved by showing that the theories are not even arithmetical. The authors do this by producing a structure \(\mathcal M\) for the language and a formula \(\nu(x)\), where \(x\) is a variable of real sort, such that \(\nu(x)\) holds in \(\mathcal M\) iff \(x\) is a natural number. However, the authors show that the \(\forall\) and \(\exists\) fragments of the theory of normed spaces is decidable along with the \(\forall\exists\) fragment of the theory of metric spaces. By reductions to Hilbert's 10th problem, they show that the \(\exists\forall\) fragments for metric spaces and normed spaces and the \(\forall\exists\) fragment for normed spaces are all undecidable.