Proving inequalities over algebraic structures

Question

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over arbitrary (semi)rings. It does this by reducing the generated polynomials to a Horner normal form and comparing equality over that.

That got me wondering whether a similar approach is possible for inequalities over general "ordered semirings" (where the order fits with the semiring operations). Someone pointed me to the omega tactic in Coq, for proving arbitrary statements (including inequalities) about Presburger arithmetic (with some restricted simulated multiplication). Anyway, it's clearly possible for Presburger arithmetic because all statements are decidable, but I don't really care about all statements, and was wondering whether it was possible for a particular algebraic structure without relying on properties of particular structures like the integers or reals.

Does anyone know whether it is possible to ? I'd be happy to even get some pointers to look more deeply into the problem, as I'm not even sure what to search for at this point.

Thanks!

Edit: there's more on the question in these slides. So I can do it on integral domains and fields through a connection with the reals. I'd really like to do it for arbitrary semirings, though.

Answer 1

The desired degree of generality seems to vary greatly among the various parts of the question and the subsequent comment. Here's a simple answer to one aspect of the question. There is no algorithm for computably enumerating all true inequalities between polynomials with natural number coefficients. (Here "true" means identically true, for all natural number values of the variables.) In particular, there is no deductive system that can prove exactly those true inequalities.

The reason is that any statement of the form "$P(x_1,\dots,x_n)$ has no integer solutions," with $P$ a polynomial over the integers, can be rewritten as an inequality between polynomials with natural number coefficients, as follows: Replace each of the integer variables $x_i$ with the difference $y_i-z_i$ of two natural number variables (so that we can talk about solutions in $\mathbb N$ instead of $\mathbb Z$); then express the absence of zeros of the polynomial as $P^2 \geq 1$; and finally, transpose any terms with negative coefficients to the right side.

Now suppose, toward a contradiction, that we could enumerate the true inequalities over the semiring $\mathbb N$. So, we could enumerate all true statements of the form "$P(x_1,\dots,x_n)$ has no integer solutions," considered above. Then we could decide whether any given Diophantine equation $P=0$ has a solution. Just run both the enumeration (to see whether it turns up a proof that there's no solution) and a systematic search for a solution. Eventually, you'll get the answer. But such a decision algorithm is impossible, by the solution of Hilbert's 10th problem.