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?

  • 1
    $\begingroup$ See the OP's related question at mathoverflow.net/q/224046/1946 $\endgroup$ – Joel David Hamkins Nov 26 '15 at 2:55
  • 1
    $\begingroup$ 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. $\endgroup$ – Joel David Hamkins Nov 26 '15 at 3:20
  • 1
    $\begingroup$ Do you want the language to include an "evaluation" operation? $\endgroup$ – Noah Schweber Nov 26 '15 at 6:34
  • 1
    $\begingroup$ 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$? $\endgroup$ – Andrej Bauer Nov 26 '15 at 11:03
  • 3
    $\begingroup$ @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. $\endgroup$ – Laurent Moret-Bailly Nov 29 '15 at 9:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.