Is being rational decidable? Given a real number uniquely defined by a finite system of equations and inequalities with rational coefficients involving the standard elementary functions only. Is it decidable whether this number is rational?
Edit: The system of equations and inequalities may have $n$ real-valued variables, and the real number to be defined is $\xi$. By decomposition using intermediate variables, we may suppose that each inequality is of the form $x_i\,\omega\, c$ where $\omega\in\{<,>,\le,\ge\}$ and $c$ is an integer, and each equation is of the form $x_i=\xi$, or $x_i=c$ where $c$ is an integer, or $x_i=x_j\circ x_k$ with $\circ\in\{+,-,*,/\}$, or $x_i=\phi(x_k)$ where $\phi\in E$ with a specified set $E$ of elementary functions, such as $E=\{\exp,\log\}$. The answer to the question might depend on the choice of $E$.
I assume that $\xi$ is uniquely determined (hence defined) by this system of equations and inequalities. One may even assume that one has a proof for this, should this help.
The algorithm may be defined according to any of various traditional models, specifying a sensible set of primitive operations (including the rational operations [e.g., on bits or on reals] and branching on an expression). I am more interested in the applicable techniques than in an answer for a particular model.
Note that the Wikipedia article on the constant problem 
claims (by reference to 
D.H. Bailey, Mathematics of Computation 50 (1988), 275–281)
a result from which decidability would follow, but this claim is spurious.
 A: This is a long comment rather than an answer.
Your problem is what is known as a "promise problem."  The input comes equipped with a promise, namely that there exists a unique real solution.  Presumably, if the promise is violated, then the algorithm is "off the hook" and can do anything it likes, including failing to halt.
I'm not aware of any research on the decidability of promise problems.  (There is some work on the computational complexity of decidable promise problems.)  The essential difficulty of your problem seems to reside in its nature as a promise problem, rather than on anything about rational numbers.  To see this, let us consider the related question: Is being an integer decidable?  This looks just as difficult as your question.
In the computational complexity realm, it's often possible to pass between promise problems and existence-of-a-solution problems.  That is, the questions "there exists a unique solution; what is it?" and "does there exist a solution?" are closely related, and one can often reduce one to the other.  Indeed, for your problem, if we had an algorithm to answer "does there exist a rational solution?" then we could solve your problem.  However, I don't see how to create a reduction in the opposite direction, because I don't see how to create suitable promise problems starting from an arbitrary system.  If we could, then perhaps the fact that Hilbert's tenth problem over $\mathbb Q$ is still open could be used to show that your problem is still open.
A: I found a paper by Babai, Just, and Meyer auf der Heide that answers a closely related question. 
They prove among others (see the discussion on p.101) that there are no anlytic computation trees (ACTs) that accept the complement of the rationals in the reals, and hence would prove the irrationality of a number.
A: As Timothy Chow pointed out, the OP's question is most naturally
formulated as a promise problem: given a finite system of
equations and inequalities in finitely many variables and the
promise that it has a solution and furthermore that all solutions
have the same value for the particular variable $\xi$, determine
whether or not that value of $\xi$ is rational.
Let me show here in various ways that if we drop the
promise-problem aspect of the problem, it is not decidable.
Theorem. There is no computable procedure to determine whether
a given finite system of equations and inequalities, allowing the
operations $+,\cdot,0,1,\sin$, has a solution in the reals.
Proof. We shall use the variables $\xi,x_1,\ldots,x_n$ and
another variable $p$. By insisting that $\sin(p)=0$ and $p>0$, we
can ensure that $p$ is an positive integer multiple of $\pi$. By
insisting that $\sin(x_i\cdot p)=0$, we can ensure that each $x_i$
is an integer.
In this way, we may transform any diophantine equation $q(\vec
x)=0$, where $q$ is polynomial in several variables over the
integers, into a system over the reals, such that $q(\vec x)=0$
has a solution over the integers if and only if the new system has
a solution over the reals.
But it is a well-known consequence of the MRDP theorem
that we cannot computably decide whether a given diophantine
equation has a solution over the integers (and this was the
solution to Hilbert's 10th problem). QED
Theorem. There is no computable procedure to determine whether
a given finite system of equations and inequalities in the
variables $x_1,\ldots,x_n,\xi$, allowing the operations
$+,\cdot,0,1,\sin$, has at least one rational value $\xi$ that is
part of a solution. Furthermore, this remains undecidable even
given the promise that there is at most one value $\xi$ that is
part of a solution, and that no irrational $\xi$ are solutions.
Proof. For any diophantine equation $q(\vec x)=0$, consider
the modified system over the reals, using the additional variable
$p$, where we insist that $q(\vec x)=0$ and also $\sin(p)=0$,
$p>0$, and $\sin(x_i\cdot p)=0$, which ensure that $p$ is a
positive integer multiple of $\pi$ and that all the $x_i$'s are
integers. Finally, add the equation $\xi=0$.
The original diophantine equation has a solution over the integers
just in case the new system has a solution over the reals, and in
any such solution, $\xi$ will be rational, because it will be $0$.
So the original system has a solution over the integers if and
only if the new system has at least one solution for which $\xi$
is rational. So this is not decidable. QED
Theorem. There is no computable procedure to determine whether
a given finite system of equations and inequalities in the
variables $x_1,\ldots,x_n,\xi$, allowing the operations
$+,\cdot,0,1,\sin$, has at most one rational $\xi$ that is part of
a solution. Furthermore, this remains undecidable under the
promise that there are at most two values of $\xi$ that solve the
system, both rational.
Proof. We use the same idea, but replace the equation $\xi=0$
with the equation $\xi(\xi-1)=0$. So this system has either no
solutions or $\xi=0$ and $\xi=1$ are both solutions. QED
These theorems do not seem to answer the full question: given a finite system of equations and inequalities, and given the promise that there is exactly one value of $\xi$ that is part of a solution, determine whether this value of $\xi$ is rational or not.
