MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top


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$

Thanks in advance!


share|cite|improve this question
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.$$


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.$$

share|cite|improve this answer

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.

Since your decision problem involves real constants, it would make sense to analyze it with some of the other infinitary notions of computability, such as Blum-Shub-Smale model, where equality of reals is decidable. And for the BSS model, I'm not sure how it comes out.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.