Some new results on decidability for elementary algebra and geometry

We carry out a systematic study of decidability for theories (a) of real vector spaces, inner product spaces, and Hilbert spaces and (b) of normed spaces, Banach spaces and metric spaces, all formalized using a 2-sorted first-order language. The theories for list (a) turn out to be decidable while the theories for list (b) are not even arithmetical: the theory of 2-dimensional Banach spaces, for example, has the same many-one degree as the set of truths of second-order arithmetic.We find that the purely universal and purely existential fragments of the theory of normed spaces are decidable, as is the ∀∃ fragment of the theory of metric spaces. These results are sharp of their type: reductions of Hilbertʼs 10th problem show that the ∃∀ fragments for metric and normed spaces and the ∀∃ fragment for normed spaces are all undecidable.