I was reading [these slides](http://www.cl.cam.ac.uk/~jrh13/slides/cmu-19mar07/slides.pdf) 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.



Real-closed fields minus existentials for Presburger-like power and multiplication?
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](http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem), which solves Hilbert's 10th problem.


