# Solving a system of equations/inequalities that have trigonometric functions on the left-hand side

Is there any known (symbolic) method that solves a system of equations/inequalities that have trigonometric functions on the left-hand side of the system?

Ex) Find $x,y,\theta \in \mathbb{R}$ that satisfy

\begin{align} 2x + y + 3\cos(\theta) - 2\sin(\theta) \le& 0 \\\ x - y + 4\cos(\theta) + 2\sin(\theta) \le& 0 \end{align}

-
This is at least as hard as 0-1 integer programming - if you set cos(x) = 0, then (1+sin(x))/2 is either 0 or 1... –  zeb Jan 27 '12 at 18:02
IF $\theta$ in the system above is bounded (e.g. between 0 and $2\pi$) then we can substitute $cos(\theta)$ with $w$ and $\sin(\theta)$ with $z$ and add an additional constraint $z^2 + w^2 = 0$. In this way we can solve the system with known methods for polynomial systems solving (e.g. cylindrical algebraic decomposition). –  SCL Jan 31 '12 at 22:47

Using, e.g., the sin function, one can write a system of inequalities in a given variable $x$ that is satisfied if and only if $x$ is an integer. Therefore, an algorithm for solving inequalities of the kind you asked about would give an algorithm of finding all integer solutions to an arbitrary system of inequalities. This would contradict the negative solution to Hilbert's Tenth Problem. See http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem

-
Thank you for your reply, SJR! Could you please give a reference for the statement: "the sin function, one can write a system of inequalities in a given variable x that is satisfied if and only if x is an integer" Or is it a trivial observation? –  SCL Jan 27 '12 at 19:08
$x$ is an integer if and only if $\sin \pi x\le 0$ and $-\sin \pi x\le 0$. Or, if you want to use only the functions $\sin x$ and $\cos x$ by themselves, you can use the inequalities $\sin z\le 0$, $-\sin z\le 0$, $z\le \pi x$ and $\pi x\le z$. –  SJR Jan 27 '12 at 19:22
Thanks, I got it. This is a sad news by the way. Have been there at least any attempts to solve this kind of systems approximately? Since cos and sin functions are important for many real-world applications, I cannot imagine that people gave up the idea of solving these systems. –  SCL Jan 27 '12 at 21:53
The metamathematics underlying the answer is that any system that is powerful enough to define the integers inside the reals is in some sense uncomputable: there is no program to determine various properties (such as being nonempty) of every finite set of inequalities so allowed. Gerhard "Ask Me About System Design" Paseman, 2012.01.27 –  Gerhard Paseman Jan 27 '12 at 23:22
On the other hand, Tarski show that certain inequality systems over the real numbers is decidable. If now you had a polynomial approximation to a trigonometric function (there may be some further technical qualifications) and were willing to work in the range where the approximation was good, then there are ways in principle (with large time complexity) to determine soutions. Gerhard "Ask Me About System Design" Paseman, 2012.01.27 –  Gerhard Paseman Jan 27 '12 at 23:26

Here's some good news to balance out the bad: If every variable that appears inside a $\sin$ or a $\cos$ is bounded, then there is something very close to a method for deciding such problems.

A basic result is that the theory of the real numbers with addition, multiplication, and the function

$S(x) = \cases{0, |x|>1\\\ \sin(x), |x|\le 1}$

is strongly model-complete. This was proved by Lou van den Dries, in a paper titled "On the Elementary Theory of Restricted Elementary Functions" (link: http://www.jstor.org/stable/2274572).

There is also an actual algorithm due to Adam Strzebonski for deciding such problems, but its correctness depends on Schanuel's conjecture, which is currently open. (link: http://dl.acm.org/citation.cfm?id=1576749.)

-
Thanks for the information zeb! My hope is that one doesn't need to resort to heavy machinery like the first-order theory of the reals, since the decision procedures are expensive. It looks like there is no better way to deal with trigonometric systems... –  SCL Jan 28 '12 at 17:04