But you did introduce multi-variable expressions, and there are some fascinating results on the multi-variable analogue of your domination problem. (Perhaps you know all this already...) That is, given two rational exponential expressions f(x1,...,xk)$f(x_1,\ldots,x_k)$ and f(x1,...,xk) $g(x_1,\ldots,x_k)$, the problem is to decide whether f(n1,...,nk) <= g(n1,...,nk) $f(n_1,\ldots,n_k)\leq g(n_1,\ldots,n_k)$, for all positive integers (n1,...,nk)$(n_1,\ldots,n_k)$ except at most finitely finitely often.
The reason is that the decision problem of Diophantine equations is encodable into this domination problem. That work famously shows that the problem to decide if a given integer polynomial p(x1,...,xk)$p(x_1,\ldots,x_k)$ has a zero in the integers is undecidable. This is the famous MRDP solution to Hilbert's 10th problem.
It is easy to reduce the Diophantine problem to the domination problem, as follows. First, let us restrict to non-negative integers, for which the MRDP results still apply. Suppose we are given a polynomial p(x1,...,xk) expression $p(x_1,\ldots,x_k)$ over the integers integers, and want to decide decide if it has a solution in the natural numbers. This expression may involve some minus signs, which your expressions do not allow, but we will take care of that by moving all the minus signs to one side. Introduce a new variable x0$x_0$ and consider the domination problem:
- Does 1 <= (1+n0)p(n1,...,nk)2$1\leq (1+n_0)p(n_1,\ldots,n_k)^2$ for all all natural numbers except finitely often?
We can expand the right hand side, and move the negative signs to the left, to arrive at an instance of your domination problem, using only positive polynomials. Now, if p(n1,...,nk)$p(n_1,\ldots,n_k)$ is never 0$0$, then the answer to the stated domination problem is Yes, since the right hand side will always be at least 1$1$ in this case. Conversely, if p(n1,...,nk) = 0$p(n_1,\ldots,n_k)=0$ has a solution, then we arrive at infinitely many violations of domination by using any choice of n0$n_0$. Thus, if we could decide the domination problem, then we could decide whether p(n1,...,nk) = 0$p(n_1,\ldots,n_k)=0$ has solutions in the natural numbers, which we cannot do by the MRDP theorem. QED
My final remark is that if one can somehow represent the inverse pairing function, then one will get undecidability even in the one variable case. That is, let f(n,m) = (n+m)(n+m+1)/2 + m$f(n,m) = \frac{(n+m)(n+m+1)}{2} + m$ be one of the usual pairing functions, which is bijective between ω2$\omega^2$ and ω$\omega$. Let p be the function such that p(f(n,m)) = n$p(f(n,m)) = n$, the projection of the pairs onto the first coordinate. If the expressions are enriched to allow p$p$, then one can in effect work with several variables by coding them all via pairing into one variable, and in this case, the domination problem in the one-variable case, for rational exponential expressions also allowing the function p$p$, will be undecidable. It would seem speculative to suppose that p$p$ is itself equivalent to a rational exponential expression, but do you know this?
