Skip to main content
1 of 3
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

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.

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.

Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k