Some new results on decidability for elementary algebra and geometry

DOI10.1016/J.APAL.2012.04.003zbMATH Open1259.03020arXiv0904.3482OpenAlexW2049594940MaRDI QIDQ714712FDOQ714712

Authors: D. Kharzeev 

Publication date: 11 October 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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 AE fragment of the theory of metric spaces. These results are sharp of their type: reductions of Hilbert's 10th problem show that the EA fragments for metric and normed spaces and the AE fragment for normed spaces are all undecidable.

Full work available at URL: https://arxiv.org/abs/0904.3482

Recommendations

• Decidability of elementary theories of certain finitely defined algebras
• scientific article; zbMATH DE number 3926284
• Decidability in elementary analysis. II
• Decidability in elementary analysis. I
• scientific article; zbMATH DE number 1263332
• On the decidability of Diophantine problems in combinatorial geometry
• New Decidable Fields of Algebraic Numbers
• A decision method for certain algebraic geometry problems
• scientific article; zbMATH DE number 4091462
• On decidable varieties of Heyting algebras

zbMATH Keywords

Hilbert spaceBanach spacedecidabilityinner product spacenormed spaceundecidability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Models of other mathematical theories (03C65) Quantifier elimination, model completeness, and related topics (03C10)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logics of metric spaces
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Undecidable theories
• Title not available (Why is that?)
• A Decision Procedure for the First Order Theory of Real Addition with Order
• Title not available (Why is that?)
• Title not available (Why is that?)
• Algorithms in real algebraic geometry
• Descriptive set theory
• Characterizations of inner product spaces
• Title not available (Why is that?)
• Title not available (Why is that?)
• Orthogonality in normed linear spaces
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quantifier elimination for modules with scalar variables
• Application of infinitary languages to metric spaces
• Solving problems by formula manipulation in logic and linear inequalities
• The Hanf Number of the First Order Theory of Banach Spaces
• Title not available (Why is that?)
• Aronszajn's criterion for Euclidean space
• Title not available (Why is that?)
• The L_ω1ω1-theory of hilbert spaces
• Title not available (Why is that?)

Cited In (12)

• A formalization of metric spaces in HOL Light
• (Dual) hoops have unique halving
• Quantifying over events in probability logic: an introduction
• Set theory and the analyst
• Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries
• Elementary invariants for quantified probability logic
• Decidability in elementary analysis. I
• Without Loss of Generality
• Decidability of the equational theory of the continuous geometry \(\mathrm{CG}(\mathbb F)\)
• Axiomatization and Undecidability Results for Metrizable Betweeness Relations
• A revision of the proof of the Kepler conjecture
• HOL Light: An Overview

This page was built for publication: Some new results on decidability for elementary algebra and geometry

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q714712)