proof theory - Proving inequalities over algebraic structures

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.