most recent 30 from http://mathoverflow.net 2013-05-22T21:40:08Z http://mathoverflow.net/feeds/question/53445 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/53445/real-closed-fields-minus-existentials-for-presburger-like-power-and-multiplicatio copumpkin 2011-01-27T03:58:57Z 2011-01-27T04:58:15Z

<p>I was reading <a href="http://www.cl.cam.ac.uk/~jrh13/slides/cmu-19mar07/slides.pdf" rel="nofollow">these slides</a> 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!)?</p> <p>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> <p>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.</p>

http://mathoverflow.net/questions/53445/real-closed-fields-minus-existentials-for-presburger-like-power-and-multiplicatio/53447#53447 Joel David Hamkins 2011-01-27T04:12:20Z 2011-01-27T04:12:20Z

<p>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 <a href="http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem" rel="nofollow">MRDP theorem</a>, which solves Hilbert's 10th problem.</p>

http://mathoverflow.net/questions/53445/real-closed-fields-minus-existentials-for-presburger-like-power-and-multiplicatio/53450#53450 SJR 2011-01-27T04:58:15Z 2011-01-27T04:58:15Z

<p>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. </p> <p>To go further than this, one must add (to the universal theory of ordered integral domains) axioms that express some special property of the ring of integers, the most obvious of which is the discreteness axiom, which asserts that there is nothing between 0 and 1. We might hope that the resulting theory (the theory of discretely ordered rings) would have a computable set of universal consequences, but this is not known. Indeed, Hilbert's Tenth Problem for discretely ordered rings is a long-standing problem for which we don't seem to have even a plausible line of attack. See for example "Which curves over Z have coordinates in a discretely ordered ring?" by van den Dries.</p>