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.

  • $\begingroup$ 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? $\endgroup$ – copumpkin Jan 27 '11 at 4:14
  • 2
    $\begingroup$ 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. $\endgroup$ – Joel David Hamkins Jan 27 '11 at 4:22
  • $\begingroup$ Disappointing, but not too surprising. Ah well, back to the drawing board :) Thanks! $\endgroup$ – 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.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.