• A complex scalar variable z can be restricted to real values by requiring $\exists z_1\exists z_2.\ z=z_1\bar{z}_1-z_2\bar{z}_2$, where z1 and z2 are fresh complex scalar variables.z=\bar{z}$. • The comparison x≤y can be replaced by$\exists z.\ x+z\bar{z}=y$, where z is a fresh complex scalar variable. Back to the original question, the following paper may be related (or even answer your question) but I do not have enough knowledge to understand the content completely. Mihai Putinar: Undecidability in a Free *-Algebra, preprint, April 2007, http://www.ima.umn.edu/preprints/apr2007/2165.pdf. 1 The second problem (with real scalar variables and the comparison relation) is equivalent to the first problem. Here is a standard argument showing this: • A complex scalar variable z can be restricted to real values by requiring$\exists z_1\exists z_2.\ z=z_1\bar{z}_1-z_2\bar{z}_2$, where z1 and z2 are fresh complex scalar variables. • The comparison x≤y can be replaced by$\exists z.\ x+z\bar{z}=y\$, where z is a fresh complex scalar variable.