3
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\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
    Commented Jan 27, 2011 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
    Commented Jan 27, 2011 at 4:22
  • $\begingroup$ Disappointing, but not too surprising. Ah well, back to the drawing board :) Thanks! $\endgroup$
    – copumpkin
    Commented Jan 27, 2011 at 4:26
2
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .