27

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.

Zakharia Stanley
  • 371
  • I believe there is such an algorithm but it's quite complicated. – Zsbán Ambrus May 03 '13 at 18:26
  • Do you have any references? – Zakharia Stanley May 03 '13 at 18:30
  • 1
    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 http://en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem – boumol May 06 '13 at 07:46
  • A related question: "Is equivalence of functions built from nested exponentiations a decidable problem?" – Laila Podlesny Nov 20 '13 at 01:21
  • Just to clarify: are you looking at expressions over the real, or the complex numbers? (I'm assuming it's the latter because of your remark about multiple-valuedness, but I just want to make sure.) – Noah Schweber Jun 14 '14 at 19:02
  • @NoahS Yes, the question is about complex numbers. We use the principal value of $a^b$, and let $a^b$ be undefined if $a=0$ and $b\le0$. – Zakharia Stanley Jun 18 '14 at 15:45
  • 1
    @StefanKohl In general, how do you evaluate the result of subtraction of two expression up to any desired precision? If the algorithm yields $0.000000...$ how do you know when to stop and if there is at least one non-zero digit? If you need the reciprocal of the difference, how do you know if it is defined at all? – Zakharia Stanley Jun 18 '14 at 15:54
  • 1
    @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
  • Similar question: http://mathoverflow.net/questions/145299/decidability-of-equality-of-elementary-expressions – André Henriques Jun 20 '14 at 19:48
  • An example: Is $3^\sqrt{5}-2^\sqrt{2}=9$? And what algorithm will solve problems of this kind? –  Dec 24 '17 at 03:51

1 Answers1

8

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

Nik Weaver
  • 42,041