Greetings,

I am wondering if there is a known decision procedure for solving the following problem, or alternately, if it is known to be undecidable.

Consider formulas that are disjunctions $F$ of parameterized arithmetic constraints, each of the form

$c_1 x_1 + c_2 x_2 + ... + c_k x_k \ge b$

where each $c_i$ is either a real constant or an unknown integer-valued parameter $p_i$, and $b$ is a real constant. The variables $x_i$ range over the reals.

Question: does there exist an instantiation of the parameters such that F is a tautology:

$\exists p_i \in \mathbb{Z}.~ \forall x_i \in \mathbb{R}.~ F$

-Swar

-
In the opening of your question, you indicate that you are concerned with a decision procedure, but your later "Question" is not about a decision procedure (but instead appears to be an instance of the desired decision problem). Perhaps it would clarify your question to phrase the matter explicitly as asking whether there is a decision procedure for the decision problem you state. –  Joel David Hamkins Oct 17 '12 at 1:42
In particular, could you specify exactly what the input for the decision problem is? I guess you mean that some of the $c_i$ are specified "real constants", but that others are integer variables $p_i$, and you want to know for a given $F$ and given constants, whether integer variables can be found to make the resulting disjunction true of all reals $x_i$. Is that right? In this case, since the input has real number data, you need to say exactly what you mean by a decision procedure. (After all, equality of real numbers, given as oracles, is not decidable.) –  Joel David Hamkins Oct 17 '12 at 2:40
(Equality of real numbers, given an algorithms computing a Cauchy sequence of rationals $\hspace{.7 in}$ and a modulus of Cauchy convergence for that sequence, is also not decidable.) $\hspace{.7 in}$ –  Ricky Demer Oct 17 '12 at 4:45

The problem is undecidable even if all the real constants $c_i$ are integers $0,\pm1$ (so that there is no issue of their representation) and all $b=0$.

By the MRDP theorem, the following problem is undecidable: given a polynomial $f\in\mathbb Z[p_1,\dots,p_l]$, determine whether there are $p_1,\dots,p_l\in\mathbb Z$ such that $f(p_1,\dots,p_l)=0$. We can rewrite $f(\vec p)=0$ as $t(\vec p)=s(\vec p)$, where $t,s$ are terms built from $p_i$ and $1$ using $+$ and $\cdot$. We can introduce extension variables for every subterm of $t$ or $s$, and replace $t=s$ with a conjunction of equations of the forms $p_i=1$, $p_i+p_j=p_k$, $p_ip_j=p_k$, and $p_i=p_j$. By manipulating the system of equations further, we can reduce it to solvability of a conjunction of formulas of the following two forms: \begin{gather*} p_i+p_j+p_k=0,\\\\ p_j\ge0\land p_ip_j+p_k=1. \end{gather*} Claim 1. Let $p_i,p_j,p_k\in\mathbb Z$.

1. $p_i+p_j+p_k=0$ if and only if for every $x,y,z\in\mathbb R$, $$p_ix-y\ge0\lor p_jx-z\ge0\lor p_kx+y+z\ge0.$$

2. $p_j\ge0\land p_ip_j+p_k=1$ if and only if for every $x,y,z,w\in\mathbb R$, $$p_ix-y\ge0\lor p_jy-z\ge0\lor p_kx-w\ge0\lor w+z-x\ge0.$$

Proof of 2 (1 is similar):

Left to right: If none of the first three inequalities hold, then $p_ix< y$, hence $p_ip_jx\le p_jy< z$, and $p_kx< w$, thus $x=(p_ip_j+p_k)x< w+z$.

Right to left: Choose a small $\epsilon>0$, and put $x=\pm1$, $y=\pm p_i+3\epsilon$, $z=\pm p_ip_j+3p_j\epsilon+\epsilon$, $w=\pm p_k+\epsilon$. Then the first three inequalities are violated, hence the fourth holds, which means that $$\pm(p_ip_j+p_k-1)+(2+3p_j)\epsilon\ge0.$$ This implies $2+3p_j\ge0$, hence $p_j\ge0$ as it is an integer, and by choosing $\epsilon$ sufficiently small we can ensure $|p_ip_j+p_k-1|< 1$, i.e., $p_ip_j+p_k-1=0$. QED

In this way, we can reduce the solvability of $f$ to solvability (for $p_1,\dots,p_r\in\mathbb Z$) of a formula of the form $$\tag{S}\bigwedge_{i=1}^n\forall x_1,\dots,x_k\in\mathbb R\bigvee_{j=1}^mL_{i,j}(x_1,\dots,x_k)\ge0,$$ where each $L_{i,j}$ is a linear function whose coefficients are either some of the parameters $p_1,\dots,p_r$, or integer constants $-1,0,1$. (In fact, the argument above gives $k=m=4$; $n$ depends on the original polynomial.) The following shows that (S) can be rewritten to the form considered in the question, hence the original problem is undecidable:

Claim 2. (S) is equivalent to $$\forall x_{1,1},x_{1,2},\dots,x_{n,k}\in\mathbb R\\,\bigvee_{e\colon\{1,\dots,n\}\to\{1,\dots,m\}}\sum_{i=1}^nL_{i,e(i)}(x_{i,1},\dots,x_{i,k})\ge0.$$

Proof:

If (S) fails, there is $i_0$ and some $x_1,\dots,x_k\in\mathbb R$ such that $L_{i_0,j}(\vec x)< 0$ for every $j$. Put $x_{i_0,j}=x_j$, and $x_{i,j}=0$ for $i\ne i_0$. Then for every $e$, we have $$\sum_{i=1}^nL_{i,e(i)}(x_{i,1},\dots,x_{i,k})=L_{i_0,e(i_0)}(x_{i_0,1},\dots,x_{i_0,k})< 0.$$ On the other hand, assume that (S) holds, and let $x_{1,1},x_{1,2},\dots,x_{n,k}\in\mathbb R$. Define $e\colon\{1,\dots,n\}\to\{1,\dots,m\}$ as follows. For any $i$, S implies that there exists $j$ such that $L_{i,j}(x_{i,1},\dots,x_{i,k})\ge0$; fix one such $j$ as $e(i)$. Then $$\sum_{i=1}^nL_{i,e(i)}(x_{i,1},\dots,x_{i,k})\ge0.$$

-
I understand your decision problem as follows: we are given finitely many real constants and a formula $F$ that is a disjunction of linear inequalities in the form you mention, having real variables $x_i$, using the specified real constants and having some unspecified integer parameters $p_i$. This instance of the decision problem is to decide yes-or-no given that data whether that formula with those real constants admit some assignment of the integer parameters making the formula universally true for all reals $x_i$.
If this is the decision problem that you meant (and please correct me if I have misunderstood), then it is not decidable. The reason is that we cannot even decide whether two real numbers $c$ and $d$ are equal (imagine giving a "yes" answer after finitely many steps of computation, which can inspect only finitely much of $c$ and $d$; one could change the reals in an uninspected part). It follows that, similarly, the question $c\leq d$ for real numbers is undecidable. But the question of $c\leq d$ is equivalent to the validity of the system $F=$ $(x\geq c)\vee(x\leq d)$' in your system, which can be expressed as $(x\geq c)\vee(-x\geq -d)$. So your decision problem is not decidable, even for instances having no integer parameters.
This argument actually shows that the decision problem of your system is not even semi-decidable, for if we could get the yes answers for validity in your system, then we could recognize positive instances of $c\leq d$, and we can already recognize instances of $d\lt c$, since any such inequality is revealed by a finite stage of inspecting $c$ and $d$, if given for example as Cauchy sequences with known convergence. Thus, by combining the two algorithms, we would be able to decide $c\leq d$, which we cannot.