# 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.

-
I see, thanks! Could you elaborate on where my line of reasoning (from integral domains to integers to nonnegative integers, assuming the slides are correct) breaks down, though? –  copumpkin Jan 27 '11 at 4:14
The decision problem in the slides seems to be whether a statement holds in all such structures, rather than just in the integers. The MRDP theorem states that you cannot decide the truth of universal statements in the integers, but perhaps you can decide whether a universal statement holds in all ordered integral domains. –  Joel David Hamkins Jan 27 '11 at 4:22
Disappointing, but not too surprising. Ah well, back to the drawing board :) Thanks! –  copumpkin Jan 27 '11 at 4:26
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.