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

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.)

• At the moment I'm not sure how adding exp/ln changes things but Tarski's theorem and a bit of work lets (with a clever encoding of division) lets you work out if two such expressions are equal absent exp/ln. Also decidability of computeable reals/algebraics doesn't matter here. You're really asking something more akin to unification or a problem in logic Doesn't mean I have an answer yet.
– Jake
May 18, 2020 at 6:49

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.

• It seems to me that Tarski's exponential function problem and the related problems are concerned about the decidability of every statement about the field expressible in first order logic, but my question is about equality, which seems more limited in scope. However, does their result imply that just the equality problem, or identity problem as they call it, is equivalent to Shaunel's Conjecture? May 18, 2020 at 8:30
• @GolDDranks, I understand ... but have you read the Richardson paper? It appears to address exactly your problem. The fact that their decision procedure relies on Shanuel's Conjecture makes me suspect it might be open whether one can decide it without that conjecture. No, their paper does not prove the two are equivalent.
– D.W.
May 18, 2020 at 15:07
• Read only the abstract this far. I'll check the paper. Thanks! May 18, 2020 at 15:39