Existential-universal quadratic arithmetic - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T04:27:10Z http://mathoverflow.net/feeds/question/109860 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/109860/existential-universal-quadratic-arithmetic Existential-universal quadratic arithmetic Swar Chaudhuri 2012-10-16T23:11:04Z 2012-10-18T11:27:27Z <p>Greetings,</p> <p>I am wondering if there is a known decision procedure for solving the following problem, or alternately, if it is known to be undecidable.</p> <p>Consider formulas that are disjunctions $F$ of parameterized arithmetic constraints, each of the form</p> <p>$c_1 x_1 + c_2 x_2 + ... + c_k x_k \ge b$</p> <p>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.</p> <p>Question: does there exist an instantiation of the parameters such that F is a tautology:</p> <p>$\exists p_i \in \mathbb{Z}.~ \forall x_i \in \mathbb{R}.~ F$ </p> <p>Thanks in advance!</p> <p>-Swar</p> http://mathoverflow.net/questions/109860/existential-universal-quadratic-arithmetic/109907#109907 Answer by Joel David Hamkins for Existential-universal quadratic arithmetic Joel David Hamkins 2012-10-17T13:35:27Z 2012-10-17T13:56:58Z <p>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$. </p> <p>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.</p> <p>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. </p> <p>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 <a href="http://en.wikipedia.org/wiki/Blum%E2%80%93Shub%E2%80%93Smale_machine" rel="nofollow">Blum-Shub-Smale model</a>, where equality of reals is decidable. And for the BSS model, I'm not sure how it comes out. </p> http://mathoverflow.net/questions/109860/existential-universal-quadratic-arithmetic/109936#109936 Answer by Emil Jeřábek for Existential-universal quadratic arithmetic Emil Jeřábek 2012-10-17T18:46:34Z 2012-10-18T11:27:27Z <p>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$.</p> <p>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*} <strong>Claim 1.</strong> Let $p_i,p_j,p_k\in\mathbb Z$.</p> <ol> <li><p>$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.$$</p></li> <li><p>$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.$$</p></li> </ol> <p><strong>Proof</strong> of 2 (1 is similar):</p> <p>Left to right: If none of the first three inequalities hold, then $p_ix&lt; y$, hence $p_ip_jx\le p_jy&lt; z$, and $p_kx&lt; w$, thus $x=(p_ip_j+p_k)x&lt; w+z$.</p> <p>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|&lt; 1$, i.e., $p_ip_j+p_k-1=0$. QED</p> <p>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:</p> <p><strong>Claim 2.</strong> (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.$$</p> <p><strong>Proof:</strong></p> <p>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)&lt; 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})&lt; 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.$$</p>