# Real-closed fields minus existentials for Presburger-like power and multiplication?

I was reading these slides by John Harrison, and was struck by the comment at the end about the universal fragment of real-closed fields needing nothing more than the axioms for an (ordered) integral domain. Since an obvious integral domain is the integers, and we can express order constraints (such as $\ge 0$) on them, does this give an algorithm for deciding universal statements on the naturals that involve addition and multiplication (by non-constants!)?

For someone interested in automatic verification of programming languages with type systems, this would be very handy if true. Can anyone provide any insight on this? I'm not a mathematician but enjoy reading about math, so I'm not positive my interpretation is correct.

P.S: I realize this is similar to my previous question, but it's more specific (and probably actually possible) so I hope to get more feedback.

The universal theory of arithmetic, in the language with $+$ and $\cdot$, is not decidable, because this is exactly sufficient to ask whether a given diophantine equation has no solutions in the integers, and this is not decidable by the MRDP theorem, which solves Hilbert's 10th problem.
The comment in the slides asserts that every ordered integral domain extends to a real closed field, or equivalently that the universal theory of real closed fields is a subset of the unversal theory of ordered integral domains. Is this useful in practice to decide whether a universal sentence is true in the integers? Sure, in the trivial sense that, e.g. the diophantine equation $x^2+y^2+1=0$ has no integer solutions because it has no solutions in any real closed field.