24

In the following definition the term expression is to be understood as a finite tree built from formal symbols without any predefined meaning assigned to them.

Define the set $\mathcal{E}$ of elementary expressions as the minimal set such that:

  • the expression $i$ is in $\mathcal{E}$
  • if $x\in\mathcal{E}$, then the expression $\exp(x)\in\mathcal{E}$,
  • if $x\in\mathcal{E}$, then the expression $\ln(x)\in\mathcal{E}$,
  • if $x,y\in\mathcal{E}$, then the expression $(x\cdot y)\in\mathcal{E}.$

Now we can assign meaning (a numeric value) to expressions in $\mathcal{E}$ as follows:

  • $i$ is the imaginary unit,
  • $\exp(x)$ is the exponent of $x$,
  • $\ln(x)$ is the principal branch of the natural logarithm of $x$ (unless the value of $x$ is zero),
  • $(x\cdot y)$ is the product of $x$ and $y$.

These rules do not assign a value to an expression if it contains a logarithm of an expression whose value is zero, e.g. $$\ln(\ln((i\cdot(i\cdot(i\cdot i))))),$$ in which case we say that the expression is invalid. Otherwise (if a value is successfully assigned), we say that the expression is valid.

Note that expressions in $\mathcal{E}$ can represent all values that can be constructed from integers and elementary functions, e.g. $\sqrt[3]{3+\sqrt2},\ \sin\frac\pi{17},\ \arctan\frac27,\ \pi^e$, etc.

Question: Is validity of expressions in $\mathcal{E}$ a decidable problem?

In other words, is there an algorithm that, given an expression $e$ in $\mathcal{E}$ as an input, always terminates and gives a correct yes/no answer indicating if the expression $e$ is valid?

Equivalent problems could be to check if a given expression is zero, or to check if two given expressions are equal to each other.

Vladimir Reshetnikov
  • 6,709
  • 6
    I am not an expert on this, but a place to start looking is Richardon's theorem, which is similar in spirit. See https://en.wikipedia.org/wiki/Richardson's_theorem – Andrej Bauer Oct 19 '13 at 22:53
  • 3
    This seems suspiciously close to other well-known problems that are open, such as Tarski's exponential function problem: http://en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem . The theory of $\mathbb{R}_{\text{exp}}$ is decidable if Schanuel's conjecture holds. – Todd Trimble Oct 19 '13 at 22:53
  • 1
    I am not sure, but since we don't have equations, it looks like a provable correct calculator. You might look at: http://prover.cs.ru.nl/calc.html. "The ProofWeb interface has been used and extended in various projects. The main ones are a prototype by Cezary Kaliszyk and Pierre Corbineau of a system that combines ProofWeb with a mathematical encyclopedia in the style of Wikipedia, and PC-Extra, an arbitrary precision calculator by Cezary Kaliszyk, based on the PhD work of Russell O'Connor. " – Lucas K. Oct 20 '13 at 22:00
  • Is it possible to give an answer to the easier question where i is replaced by 1, i.e. one considers as expressions: 1; exp(x); ln(x); (x⋅y) ? – abo Oct 21 '13 at 19:20
  • The reference you give does not really explain what a principal branch of the log is. Usually, the principal branch means that we take the cut on the negative ray. Then how $\log(-1)$ is defined in your question? – Alexandre Eremenko Nov 16 '13 at 23:39
  • @AlexandreEremenko $\ln\left(-1\right)=\pi,\sqrt{-1}=\pi,i$ – Vladimir Reshetnikov Nov 17 '13 at 20:50
  • I agree with Todd. A toy example: does $e^e+5=e^3?$ And more generally: how accurately do you need to calculate two expressions in $\mathcal{E}$ to decide whether they are equal? –  Dec 30 '13 at 00:45
  • 1
    Similar question: http://mathoverflow.net/questions/129563/decidability-of-equality-of-expressions-built-using-1 – André Henriques Jun 20 '14 at 19:48
  • @abo, my example above can also be written as $e^{e^e}e e e e e=e^{e e e}$, which is of the form you suggest. So, even for that limited form, I think no algorithm for deciding sentences of that form has been proved correct. –  Sep 06 '21 at 05:47
  • Another very similar question: https://mathoverflow.net/q/118972/17064 – Gro-Tsen Sep 06 '21 at 15:54

1 Answers1

1

$\mathcal{E}$ is the set of the explicit elementary numbers. The explicit elementary numbers can be generated from the rational numbers by applying finite numbers of $\exp$, $\ln$ and/or explict algebraic functions.

The set that is generated from a complex variable by applying finite numbers of $\exp$, $\ln$ and/or (explict and/or implicit) algebraic functions, are the elementary functions (of Liouville and Ritt).

[Risch 1979] proves a structure theorem for the elementary functions and gives a corresponding algorithm.
$\ $

[Risch 1979] Risch, R. H.: Algebraic Properties of the Elementary Functions of Analysis. Amer. J. Math 101 (1979) (4) 743-759

IV_
  • 1,063
  • 3
    The article by Risch gives an algorithm “provided the algebraic structure of the field generated over Q by the complex numbers appearing in the following process is known” (p. 750); “we believe the algorithm will work in most practical situations. However, its universal applicability depends on the solution of some extremely difficult problems in the theory of transcendental numbers.” (p. 744) So the paper may leave this question open. It would help if Risch had provided at least one example of applying the algorithm — I can not tell causally if it works even for my toy example of $e^3=e^e+5$. –  Aug 21 '21 at 23:21