Tarski's theorem on real-closed fields shows that there is a decision procedure to compute the truth or falsity of any first-order statement in the real closed field $\lanagle\mathbb{R},+,\cdot,\lt,0,1\rangle$, which includes via Cartesian geometry many of the usual concepts of Euclidean geometry and more. For example, this language is expressive enough to speak of circles, lines, paraboloids, and so on, real algebraic equations in any finite dimension, the $n$-dimensional metric, concepts of bounded or unbounded solution sets and so on. Tarski's algorithm provably determines the truth of any statement expressible in this language, even when these statements involve complex alternations of quantifiers (for every circle, there are three lines such that for every parabola of a certain kind and so on...), which in other contexts often cause undecidability.

Unfortunately, the set of integers is not definable in this language (since this would immediate refute decidability by allowing the halting problem to be expressed), and it follows that Tarski's theorem does not apply very well to questions about algorithms, which is the main focus of your question, since one seems to need the integers to express concepts of iterating a procedure, a central consideration with algorithms.

Tarski's theorem on real-closed fields shows that there is a decision procedure to compute the truth or falsity of any first-order statement in the real closed field $\langle\mathbb{R},+,\cdot,\lt,0,1\rangle$, which includes via Cartesian geometry many of the usual concepts of Euclidean geometry and more. For example, this language is expressive enough to speak of circles, lines, paraboloids, and so on, real algebraic equations in any finite dimension, the $n$-dimensional metric, concepts of bounded or unbounded solution sets and so on. Tarski's algorithm provably determines the truth of any statement expressible in this language, even when these statements involve complex alternations of quantifiers (for every circle, there are three lines such that for every parabola of a certain kind and so on...), which in other contexts often cause undecidability.

Unfortunately, the set of integers is not definable in this language (since this would immediate refute decidability by allowing the halting problem to be expressed), and it follows that Tarski's theorem does not apply very well to questions about algorithms, which is the main focus of your question, since one seems to need the integers to express concepts of iterating a procedure, a central consideration with algorithms.