MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 Meh, I can't make up my mind about the title

1

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