Decidability of equality, and soundness of expressions involving elementary arithmetic and exponentials

Question

Let's have expressions that are composed of elements of $\mathbb N$ and a limited set of binary operations {$+,\times,-,/$} and functions {$\exp, \ln$}. The expressions are always well-formed and form finite trees, with numbers as leaf nodes and operators as internal nodes, binary operations having two child sub-expressions and the functions one. A value of such an expression is interpreted to mean some number in $\mathbb R$.

There are two limitations on the structure of the expressions: the divisor (the right-hand sub-expression) of $/$ can't be 0 and the argument of $\ln$ must be positive.

I have two questions about these kind of expressions:

• Is it possible to ensure "soundness" of such an expression, in the sense that the two limitations can be checked in finite time?

• is an equality check between two such expressions decidable?

These questions seem to be connected in the sense that if you're able to check equality of the relevant sub-expression to zero, you can decide whether a division parent expression is sound, and it doesn't seem hard to check whether a sub-expression of $\ln$ is positive or negative if it's known not to be zero.

I know that equality in $\mathbb R$ is generally not decidable, whereas equality in algebraic numbers is. However, I wonder how inclusion of {$\exp, \ln$} changes the result. I suspect that if there exists "pathological cases" where two expressions with dramatically different structure result to the same real number, checking the equality between them might be undecidable, as the $\exp$ and $\ln$ might hinder the normalization of such expressions.

(A side note: I posted an earlier version of a question with similar intent here, but it turned out to have too little thought behind it, and had unnecessary (= not related to the meat of the question) complications with complex logarithms.)

Answer 1

I don't know, but I suspect it's an open question.

If the theory of the reals with exponential function is decidable, then your problem is decidable, too. It is known that if Shanuel's Conjecture holds, then the former is decidable, so your problem is too.

If I understand correctly, the following paper tackles your problem:

The identity problem for elementary functions and constants. Dan Richardson, John Fitch. ISSAC '94.

It appears that they show a procedure that always terminates if Shanuel's Conjecture holds; and if it doesn't terminate for a particular expression, then we can extract from that expression a counterexample to Shanuel's Conjecture. They then argue that it seems unlikely that we will find a counterexample any time soon, so it seems unlikely we will find inputs on which this procedure fails to terminate any time soon.

See also https://mathoverflow.net/q/118972/37212 and https://mathoverflow.net/q/129563/37212 and https://mathoverflow.net/q/145299/37212.