Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
    
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
    
add comment

1 Answer

The equational theory of $\langle {\bf N}, 0, 1, +, \times, \uparrow\rangle$ is decidable, but not finitely axiomatizable.

share|improve this answer
4  
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
    
That's right, I agree. –  Nik Weaver May 3 '13 at 19:11
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.