Some new results on decidability for elementary algebra and geometry

Robert M. Solovay, R.D. Arthan, John Harrison. Annals of Pure and Applied Logic, vol. 163, pp. 1765-1802, 2012.

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:

@ARTICLE{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",
        journal         = "Annals of Pure and Applied Logic",
        volume          = 163,
        year            = 2012,
        pages           = "1765--1802"}