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

(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 negative logarithms.)