# Existential Theory of the Reals in NP?

It is known that the existential theory of the reals is decidable in PSPACE (via John Canny), but as far as I can tell no one has demonstrated that it is in NP. This confuses me because it seems like a short certificate for a given formula would be an example of values for the variables included in the formula that demonstrates a valid assignment. Why is this argument invalid?

• I suggest you look at this problem. Mar 24, 2018 at 0:39

No, unfortunately that doesn't work. The certificate needs to be a sequence of bits that is verifiable in polynomial time -- and thus the length of the certificate has to be at most a polynomial in the length of the input instance. If your certificate is the value of some variables, and those values are real numbers, you might not be able to write down their binary representation in any reasonable amount of space (indeed, their binary representation might be infinite-length).

For instance, consider the sentence $\exists x . x^2 = 2$. This sentence is valid, as $x= \sqrt{2}$ is an example that makes $x^2=2$ true. However, when you try to write out $\sqrt{2}$ in binary, you get an infinite sequence, so it's not clear what the short certificate would be. (Certificates need to be of finite length, certainly.) In general, representing real numbers in binary is messy business; no matter what representation you choose, there will always be some real numbers you can't represent finitely.

• The existential theory does not include universal qualifiers, so the first point you raise is not relevant. For the second point, if the values in question are expressed in unary (and are constrained to the computable numbers) do we then get a NP certificate? Mar 23, 2018 at 23:39
• @nick.schachter, oops, you're right, sorry about that. I've edited my answer. Nope, expressing them in unary isn't enough. See the example I added to illustrate why.
– D.W.
Mar 24, 2018 at 0:55
• But does not this argument contradict the fact that $\exists\mathbb R\subseteq \mathsf{PSPACE}$? Mar 24, 2018 at 0:59
• @rus9384, no, I don't think so. Why would it? All I'm saying is "that's not a valid argument that the problem is in NP". Why would that imply anything more? Not all problems in PSPACE are also in NP (and just because one argument that the problem is in NP is invalid doesn't mean there aren't other valid arguments).
– D.W.
Mar 24, 2018 at 1:31
• I mean that there solution must be computable with polynomial space usage, while converting reals to binary strings is undecidable. On the other hand given problem is as hard as geometric quantum logic, which is, I guess, $\mathsf{QMA}$-hard. Mar 24, 2018 at 1:40