# Is the positive existential theory undecidable?

Could you tell if the positive existential theory of $\mathbb{C}[e^{\mu x} \mid \mu \in \mathbb{C}]$ is undecidable in the language $\{+, \cdot , \frac{d}{dx} , 0, 1, e^x\}$ ?

How can we prove the (un)decidability?

• See the OP's related question at mathoverflow.net/q/224046/1946 – Joel David Hamkins Nov 26 '15 at 2:55
• The way you ask the question suggests that you somehow know already that it is undecidable (since you ask how we could prove this, rather than whether it is true). But is that right--are you claiming to know already that it is undecidable? If not, I'd suggest editing the question to use a different wording. – Joel David Hamkins Nov 26 '15 at 3:20
• Do you want the language to include an "evaluation" operation? – Noah Schweber Nov 26 '15 at 6:34
• He means: "is there an operation $ev$ which allows us to set the value of $x$" so that for example we can do $ev(e^x, 4)$ which then equals $e^4$? – Andrej Bauer Nov 26 '15 at 11:03
• @MaryStar: I am not sure what you mean by "have to". What you have to do is state your problem(s) in precise terms. The point of my (and other people's) comments is that you get different problems by including (or not) some sort of evaluation function in your language. All these problems may be interesting. – Laurent Moret-Bailly Nov 29 '15 at 9:07