# Decidability of equality of expressions built using 1,+,-,*,/,^

Consider expressions built using number $1$, arithmetical operators $+, -, *, /$ and exponentiation ^ (in case of multiple values, the principal value is assumed, the same way as it implemented in Power function in Mathematica). Is it a decidable problem to check if such an expression is zero? If so, could you please point me to an algorithm that can solve this problem?

Update: I found a reference to Richardson's Theorem, that establishes undecidablity of equality in a wider set of expressions, in particular, including the logarithm and absolute value functions.

-
I believe there is such an algorithm but it's quite complicated. – Zsbán Ambrus May 3 '13 at 18:26
Do you have any references? – Zakharia Stanley May 3 '13 at 18:30
If you are thinking on variables just taking values over real numbers it is known that the full first-order theory is decidable under Schanuel's conjecture. You can find more information in en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem – boumol May 6 '13 at 7:46
– Laila Podlesny Nov 20 '13 at 1:21
@ZakhariaStanley: Sorry, I made a mistake in my tentative argumentation. -- I removed my comment. Though I think the question essentially is whether the value of an expression of length $n$ as described in the question is bounded above by a computable function in $n$ or not. – Stefan Kohl Jun 18 '14 at 16:25

Thanks for the reference. But it looks like a different problem. The division operator $/$ takes it beyond integers and, together with $-$ and ^, beyond reals and algebraics. – Zakharia Stanley May 3 '13 at 18:54