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.