Some new results on decidability for elementary algebra and geometry

Robert M. Solovay, R.D. Arthan, John Harrison. ArXiV preprint 0904.3482, submitted to Annals of Pure and Applied Logic, 2009.

Abstract:

Abstract We carry out a systematic study of decidability for theories of (a) real vector spaces, inner product spaces, and Hilbert spaces and (b) normed spaces, Banach spaces and metric spaces, all formalised 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 Hilberts 10th problem show that the ∃∀ fragments for metric and normed spaces and the ∀∃ fragment for normed spaces are all undecidable.

PDF

Bibtex entry:

@UNPUBLISHED{solovay-arthan-harrison,
        author          = "Robert M. Solovay and R.D. Arthan and
                           John Harrison",
        title           = "Some new results on decidability for
                           elementary algebra and geometry",
        note            = "ArXiV preprint 0904.3482; submitted to
                           Annals of Pure and Applied Logic. Available at
 {\url{http://arxiv.org/PS_cache/arxiv/pdf/0904/0904.3482v1.pdf}}",
        year            = 2009}