Existential-universal quadratic arithmetic - MathOverflow

Existential-universal quadratic arithmetic

2012-10-16T23:11:04Z

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$

Thanks in advance!

-Swar

Answer by Joel David Hamkins for Existential-universal quadratic arithmetic

2012-10-17T13:35:27Z

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.

Answer by Emil Jeřábek for Existential-universal quadratic arithmetic

2012-10-17T18:46:34Z

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

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