Pseudo-Complex Quantifier Elimination
April 29, 2026
Abstract
We describe the design of a quantifier elimination framework for the complex numbers in the language of ordered rings supplemented with symbols for the imaginary unit, real parts, imaginary parts, and conjugates. Technically, we use a reduction to real quantifier elimination followed by a heuristic reinterpretation of the results within our complex framework. We present computational examples using a prototypical implementation of our approach in our Python-based open-source system Logic1.
1 Introduction↩︎
Based on research conducted during the 1930s [1], Tarski published the first complete quantifier elimination (qe) procedure for the real numbers in 1948 [2]. Subsequent work by Seidenberg in 1954 provided a geometric interpretation of these results, known today as the Tarski–Seidenberg Theorem [3], which naturally gives rise to the idea of applying these methods to real-world problems. Remarkably, concluding remarks in a 1954 report to the US Army by Davis already address the infeasibility of implementing real qe, indicating early interest in the problem [4]. Given the state of the available programming infrastructure at the time, along with the fact that the Tarski–Seidenberg procedure is not even elementary recursive in the worst case, Davis’s assessment was certainly justified. This picture began to change during the 1970s, when Collins and his students developed and implemented real qe methods based on cylindrical algebraic decomposition (cad) [5]. In the mid-1980s partial cad constituted a major breakthrough [6]. Complemented with more specialized virtual substitution methods aimed at formulas of low degree [7]–[9], real qe became applicable to a considerable number of application areas with a significant publication record, also at the CASC conference series. Another class of implemented approaches to real qe is based on multivariate parametric real root counting [10]–[12].
The early history of qe for the ring of complex numbers resembles that of real qe outlined above. It was again Tarski who developed a first qe procedure during the 1940s, without explicitly publishing it at the time [13]. With his famous theorem on the constructability of images, Chevalley contributed a geometric perspective on Tarski’s result for the complex numbers, resembling Seidenberg’s work for the reals [14]. As in the real case, Tarski’s procedure is not elementary recursive. A more modern approach, implemented in Redlog [15], is based on comprehensive Gröbner bases [16]. More generally, complex qe is supported in computer algebra systems through algebraic decomposition techniques. In particular, Maple’s Regular Chains library [17] provides functionality for manipulating constructible sets and computing projections via triangular decomposition [18]. Other systems such as Singular, Magma, and Macaulay2 offer the necessary elimination primitives, but require manual construction of qe procedures.
When focusing on rigorous logical settings, real qe is currently much better supported in software than complex qe, and numerous applications have been documented in the scientific literature; see, e.g., [11], [19], [20] and the references therein. One recent line of research focuses on the qualitative analysis of chemical reaction networks, e.g., [21]. A major reason for the stronger interest in real qe is that classical complex qe in the language of rings lacks symbols naturally expected by users in the natural sciences and engineering, namely a constant for the imaginary unit, as well as operators for the real and imaginary parts and for complex conjugation. In fact, the addition of these symbols implicitly reduces the problem to real qe, as is essentially known in the community. Our work makes this approach explicit by providing a formal qe procedure in the extended language, which we call pseudo-complex quantifier elimination.
Our original contributions are the following:
We formally introduce terms and first-order formulas, define various relevant syntactic normal forms, and provide a rigorous formal semantics. (Sections 2 and 3)
We reduce qe for our framework to real qe. We furthermore prove that the first-order theory corresponding to our framework is complete and decidable. (Section 4)
Building on real qe, we obtain qe results with terms inductively constructed from rational constants and the real and imaginary parts \(\Re(z)\) and \(\Im(z)\) of complex variables \(z\), exclusively using ring operations. We introduce graph-based heuristics to produce equivalent, more compact results in the unrestricted language and prove complexity bounds for these heuristics. (Section 5)
We give asymptotic complexity bounds for our qe, which coincide with the known bounds for classical real and complex qe. From a practical perspective, our approach makes existing real qe software accessible for problems over complex numbers. (Section 6)
We have implemented our approach in our Python-based open-source system Logic1. A number of computation examples demonstrate the practical applicability of our approach. (Section 7)
We finally summarize and evaluate our results in Section 8.
2 Language, Terms and Normal Forms↩︎
We use the countably infinite language of ordered rings along with constant symbols for all non-negative rational numbers, plus another constant symbol for the imaginary unit, plus further unary function symbols for the real part, the imaginary part, and the conjugate: \[\mathcal{L}= \bigl\{\, q^{(0)},\, +^{(2)},\, -^{(1)},\, \mathbin{{\, \cdot \, }}^{(2)},\, \mathord{\mathrm{i}}^{(0)},\, \Re^{(1)},\, \Im^{(1)},\, \overline{\,\cdot\, }^{(1)};\, <^{(2)},\, \leq^{(2)},\, \neq^{(2)} \,\bigm\vert\, q \in \mathbb{Q}_{\geqslant 0} \, \bigr\}.\] Note that ‘\(<\)’, ‘\(\leq\)’, and ‘\({\neq}\)’ are relation symbols, while all other symbols in \(\mathcal{L}\) are function symbols, including constant symbols. Numbers in parentheses indicate the arities of respective symbols. We furthermore fix a countably infinite, strictly ordered set \((\mathcal{V}, \prec)\) of variables. As usual, terms are built inductively, starting with constant symbols and variables and applying non-constant function symbols, respecting their arities. This yields the countably infinite set \(\mathcal{T}\) of all terms with function symbols from \(\mathcal{L}\) and variables from \(\mathcal{V}\).
Let \(n \in \mathbb{N}\) and \(z_1\), …, \(z_n \in \mathcal{V}\) with \(z_1 \prec \dots \prec z_n\), and set \(\mathbf{z}= (z_1, \dots, z_n)\). We write \(\mathcal{T}_\mathbf{z}\subseteq \mathcal{T}\) for the set of all terms over variables in \(\mathbf{z}\).
Consider \(t \in \mathcal{T}\) and let \(\{z_1, \dots, z_n\} \subseteq \mathcal{V}\) be a superset of the variables occurring in \(t\). Then \(t(z_1, \dots, z_n)\) is called an extended term. Each extended term induces an interpretation \(t(z_1, \dots, z_n)^*: \mathbb{C}^n \to \mathbb{C}\). Two terms \(t_1\), \(t_2 \in \mathcal{T}_\mathbf{z}\) are equivalent if \(t_1(\mathbf{z})^* = t_2(\mathbf{z})^*\). We then write \(t_1 \approx t_2\).
Remark 1 (Universal statements about extended terms). For \(t_1\), \(t_2 \in \mathcal{T}_\mathbf{z}\) the following are equivalent:
\(t_1 \approx t_2\);
\(t_1(\mathbf{z}')^* = t_2(\mathbf{z}')^*\) for at least one \(m \in \mathbb{N}\) and \(\mathbf{z}' \in \mathcal{V}^m\) such that both \(t_1(\mathbf{z}')\) and \(t_2(\mathbf{z}')\) are extended terms;
\(t_1(\mathbf{z}')^* = t_2(\mathbf{z}')^*\) for all \(m \in \mathbb{N}\) and \(\mathbf{z}' \in \mathcal{V}^m\) such that both \(t_1(\mathbf{z}')\) and \(t_2(\mathbf{z}')\) are extended terms.
The reason is that modification of the extension by permutation, addition, or removal of variables not occurring in \(t_1\), \(t_2\) does not affect the universal statement about all possible complex arguments in the definition of term equivalence.0◻
We call \(\mathcal{N}_\mathbf{z}\subseteq \mathcal{T}_\mathbf{z}\) a system of normal forms for \(\mathcal{T}_\mathbf{z}\) if for each \(t \in \mathcal{T}_\mathbf{z}\) there is \(t' \in \mathcal{N}_\mathbf{z}\) with \(t' \approx t\). We call \(\mathcal{N}_\mathbf{z}\) a system of unique normal forms if there is exactly one such \(t'\) for each \(t\).
Let \(t_1\), …, \(t_n \in \mathcal{T}\). As usual, we agree that multiplication has higher precedence than addition. Furthermore, we shortly write \(t_1 + \dots + t_n\) and \(t_1 \cdots t_n\) for iterated left-associative application of addition and multiplication, respectively. Finally, exponentiation \(t_1^m\) denotes \(m\)-fold multiplication for \(m \geq 2\).
Denote by \(\mathbb{Q}[\mathord{\mathrm{i}}]\) the algebraic extension ring, whose elements can be uniquely written as linear polynomials \(q_1\mathord{\mathrm{i}}+ q_2\) with \(q_1\), \(q_2 \in \mathbb{Q}\). We note that \(\mathbb{Q}[\mathord{\mathrm{i}}]\) is even a field, which equals the extension field \(\mathbb{Q}(\mathord{\mathrm{i}})\). On these grounds, we specify conjugate normal forms \(\mathcal{N}^-_\mathbf{z}\) and Cartesian normal forms \(\mathcal{N}^+_\mathbf{z}\) for \(\mathcal{T}_\mathbf{z}\) as follows.
Proposition 1 (Conjugate normal form). Consider \(\mathcal{T}_\mathbf{z}\) with \(\mathbf{z}\in \mathcal{V}^n\) for \(n \in \mathbb{N}\). Define the polynomial ring \(R = \mathbb{Q}[\mathord{\mathrm{i}}][z_1, \dots, z_n, \overline{z_1}, \dots, \overline{z_n}]\) with \(2n\) algebraically independent generators. Let \(\mathcal{N}^-_\mathbf{z}\subseteq \mathcal{T}_\mathbf{z}\) be the set of terms corresponding to polynomials in \(R\) using linear polynomial coefficients and degree-lexicographic order. Then \(\mathcal{N}^-_\mathbf{z}\) is a system of unique normal forms for \(\mathcal{T}_\mathbf{z}\).
Proof. Let \(t \in \mathcal{T}_\mathbf{z}\). We transform \(t\) in three subsequent steps as follows:
Equivalently rewrite subterms of \(t\) as follows, where \(s_1\) does not contain \(\Re\) and \(s_2\) does not contain \(\Im\): \[\Re(s_1) \to \frac{1}{2} \cdot (s_1 + \overline{s_1}), \quad \Im(s_2) \to -\frac{1}{2} \cdot \mathord{\mathrm{i}}\cdot (s_2 - \overline{s_2}).\] This procedure terminates and yields \(t' \in \mathcal{T}_\mathbf{z}\) with \(t' \approx t\), and \(t'\) does not contain \(\Re\), \(\Im\).
In \(t'\), equivalently propagate complex conjugates inwards by rewriting subterms as follows: \[\begin{align} &\overline{s_1 + s_2} \to \overline{s_1} + \overline{s_2},\quad \overline{s_1 \cdot s_2} \to \overline{s_1} \cdot \overline{s_2},\quad & s_1, s_2 &\in \mathcal{T}_\mathbf{z},\\ &\overline{-s} \to -\overline{s},\quad \overline{\overline{s}} \to s, & s &\in \mathcal{T}_\mathbf{z},\\ &\overline{q} \to q, & q &\in \mathbb{Q}_{\geqslant 0},\\ &\overline{\mathord{\mathrm{i}}} \to -\mathord{\mathrm{i}}. \end{align}\] This procedure terminates and yields \(t'' \in \mathcal{T}_\mathbf{z}\) with \(t'' \approx t\), and \(t''\) is exclusively built from variables, constant symbols, conjugates of variables, and ring operator symbols.
We equivalently expand \(t''\) into a polynomial \(t''' \in R\) with \(t''' \approx t\), using the laws of arithmetic of commutative rings.
Uniqueness of \(t'''\) follows from the observation that the set \[\bigl\{\,z_1^{e_1} \cdots z_n^{e_n}\cdot \overline{z_1}^{e_{n+1}} \cdots \overline{z_n}^{e_{2n}}(\mathbf{z})^* \bigm| \mathbf{e}\in \mathbb{N}^{2n}\,\bigr\}\] is linear independent in the vector space of functions from \(\mathbb{C}^n\) to \(\mathbb{C}\), so that our normal forms are identical zero as functions if and only if they are formally equal to zero. ◻
Note that we can obtain alternative unique conjugate normal forms for \(\mathcal{T}_\mathbf{z}\) by using other monomial orders instead of the degree-lexicographic order.
Proposition 2 (Cartesian normal norm). Consider \(\mathcal{T}_\mathbf{z}\) with \(\mathbf{z}\in \mathcal{V}^n\) for \(n \in \mathbb{N}\). Define the polynomial ring \(S = \mathbb{Q}[\Re(z_1), \dots, \Re(z_n), \Im(z_1), \dots, \Im(z_n)]\) with \(2n\) algebraically independent generators. Let \(\mathcal{N}^+_\mathbf{z}= \{\, p_1 + \mathord{\mathrm{i}}\cdot p_2 \in \mathcal{T}_\mathbf{z}\mid p_1, p_2 \in S\,\}\) using degree-lexicographic order for \(p_1\) and \(p_2\) and omitting summands \(0\) and factors \(1\) as usual. Then \(\mathcal{N}^+_\mathbf{z}\) is a system of unique normal forms for \(\mathcal{T}_\mathbf{z}\).
Proof. Let \(t \in \mathcal{T}_\mathbf{z}\), without loss of generality \(t \in \mathcal{N}^-_\mathbf{z}\). Recall from Proposition 1 that \(t\) corresponds to a polynomial in \(\mathbb{Q}[\mathord{\mathrm{i}}][\mathbf{z}, \overline{\mathbf{z}}]\), where the coefficients are represented as linear polynomials in \(\mathord{\mathrm{i}}\). We proceed in three steps:
Denote \(\mathbf{z}= (z_1, \dots, z_n)\) and rewrite the monomials of \(t\) as follows: \[\prod_{i=1}^n z_i^{e_i} \cdot \prod_{i=1}^n \overline{z_i}^{e_{n + i}}\to \prod_{i=1}^n \bigl(\Re(z_i) + \mathord{\mathrm{i}}\cdot\Im(z_i)\bigr)^{e_i} \cdot \prod_{i=1}^n \bigl(\Re(z_i) - \mathord{\mathrm{i}}\cdot\Im(z_i)\bigr)^{e_{n + i}}.\] This yields \(t' \in \mathcal{T}_\mathbf{z}\) with \(t' \approx t\), and \(t'\) is exclusively built from constant symbols, subterms \(\Re(z_i)\), \(\Im(z_i)\), and ring operator symbols.
Equivalently expand \(t'\) into a polynomial \[t'' \in \mathbb{Q}[\mathord{\mathrm{i}}][\Re(z_1), \dots, \Re(z_n), \Im(z_1), \dots, \Im(z_n)]\] with \(t'' \approx t\), using the laws of arithmetic of commutative rings.
Using the laws of arithmetic of commutative rings once again, it is straightforward to equivalently transform \(t''\) into \(t''' \in \mathcal{N}^+_\mathbf{z}\).
For uniqueness, it is sufficient to show that our normal forms \(t'''\) are pairwise not equivalent. Consider \(t_1'''\), \(t_2'''\) with \(t_1''' \neq t_2'''\). According to our construction, there are \(t_1\), \(t_2\) in conjugate normal form with \(t_1 \neq t_2\) and \(t_1''' \approx t_1\) and \(t_2''' \approx t_2\). By the uniqueness of the conjugate normal form, we know that \(t_1 \not\approx t_2\), hence \(t_1''' \approx t_1 \not\approx t_2 \approx t_2'''\). ◻
Similarly to \(\mathbb{Q}[\mathord{\mathrm{i}}][\mathbf{z}, \overline{\mathbf{z}}]\) above, we will shortly write \(\mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\) from now on. Again, we can obtain alternative unique Cartesian normal forms for \(\mathcal{T}_\mathbf{z}\) by using other monomial orders instead of the degree-lexicographic order. We furthermore note that Cartesian normal forms of arbitrary terms can be more efficiently computed directly instead of going via conjugate normal forms. In the symbols \(\mathcal{N}^-_\mathbf{z}\) and \(\mathcal{N}^+_\mathbf{z}\), the ‘\(-\)’ and the ‘\(+\)’ point at the conjugate operation and the Cartesian coordinate system, respectively.
Example 1 (Conjugate and cartesian normal forms). Consider \[\begin{align} s_1 & = z^2+ \mathord{\mathrm{i}}, & t_1 & = \bigl(\Re(z)^2 - \Im(z)^2\bigr) + \mathord{\mathrm{i}}\cdot \bigl(2\Re(z)\Im(z) + 1\bigr),\\ s_2 & = z\overline{z}, & t_2 & = \Re(z)^2 + \Im(z)^2,\\ s_3 & = 2\mathord{\mathrm{i}}+ 1, & t_3 &= 1 + \mathord{\mathrm{i}}\cdot 2. \end{align}\] For \(i \in \{1, \dots, 3\}\), we have \(s_i \approx t_i\), where \(s_i\) is in conjugate normal form, and \(t_i\) is in Cartesian normal form.
We call \(t \in \mathcal{T}_\mathbf{z}\) a real term if \(t(\mathbf{z})^*[\mathbb{C}^n] \subseteq \mathbb{R}\). This is equivalent to the requirement that \(t(\mathbf{z}')^*[\mathbb{C}^m] \subseteq \mathbb{R}\) for all extended terms \(t(\mathbf{z}')\) with \(\mathbf{z}' \in \mathcal{V}^m\); compare Remark 1.
Proposition 3 (Characterization of real terms). Let \(t \in \mathcal{T}_\mathbf{z}\) with \(\mathbf{z}\in \mathcal{V}^n\) for \(n \in \mathbb{N}\). Then the following are equivalent:
\(t\) is a real term;
\(\Im(t) \approx 0\);
the Cartesian normal form of \(t\) is a polynomial in \(\mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\).
Proof. We denote by \(\Re^*: \mathbb{C}\to \mathbb{C}\) the real part, by \(\Im^*: \mathbb{C}\to \mathbb{C}\) the imaginary part, and by \(\mathord{\mathrm{i}}^* \in \mathbb{C}\) the imaginary unit.
Assume (iii), that is \(t \approx t'\) with \(t' \in \mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\), and let \(\mathbf{c}\in \mathbb{C}^n\). Since \(\Re^*[\mathbb{C}] = \mathbb{R}\), \(\Im^*[\mathbb{C}] = \mathbb{R}\), and \(\mathbb{R}\subseteq \mathbb{C}\) is closed under ring arithmetic, we obtain \(t(\mathbf{z})^*(\mathbf{c}) = t'(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}\). We have thus shown (i).
Assume (i), that is \(t(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}\), and let \(\mathbf{c}\in \mathbb{C}^n\). It follows that \[\Im(t)(\mathbf{z})^*(\mathbf{c}) = \Im^*(t(\mathbf{z})^*(\mathbf{c})) = 0 = 0(\mathbf{z})^*(\mathbf{c}),\] and we have shown (ii).
Assume (ii), and let \(f\), \(g \in \mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\) be the unique choices such that \(t \approx f + \mathord{\mathrm{i}}\cdot g\). Using the same arguments as in our proof step from (iii) to (i) above, we conclude that \(f(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}\) and \(g(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}\) for all \(\mathbf{c}\in \mathbb{C}^n\). Assume for a contradiction that \(g \neq 0\). Then there exists \(\mathbf{c}\in \mathbb{C}^n\) such that \(g(\mathbf{z})^*(\mathbf{c}) \neq 0\), and we obtain \[\Im(t)(\mathbf{z})^*(\mathbf{c}) = \Im^*(t(\mathbf{z})^*(\mathbf{c})) = \Im^*(f(\mathbf{z})^*(\mathbf{c}) + \mathord{\mathrm{i}}^*g(\mathbf{z})^*(\mathbf{c})) = g(\mathbf{z})^*(\mathbf{c}) \neq 0(\mathbf{z})^*(\mathbf{c}),\] which contradicts (ii). Hence \(g = 0\), and we have shown (iii). ◻
Note that property (ii) in the previous lemma can be checked via normal form computation on \(t\), using any system of unique normal forms of terms.
3 Atoms and First-order Formulas↩︎
Given \(t_1\), \(t_2\), \(r_1\), \(r_2 \in \mathcal{T}\), where \(r_1\), \(r_2\) are real terms, atomic formulas, or atoms for short, are of one of the following forms: \[t_1 = t_2, \quad t_1 \neq t_2, \quad r_1 \leq r_2, \quad r_1 < r_2,\] where, as usual in interpreted first order logic, the equal sign is not an element of the language \(\mathcal{L}\). This yields the countably infinite set \(\mathcal{A}\) of all atoms. Note that we permit ‘\(<\)’ and ‘\(\leq\)’ to be used only with real terms. Our software will recognize other uses via Proposition 3 and raise an exception.
As usual, quantifier-free formulas are built inductively, starting with atoms and the constant formulas \(\top^{(0)}\) (‘true’), \(\bot^{(0)}\) (‘false’), and applying non-constant logical operators \[\lnot^{(1)},\quad \mathrel{\land}^{(*)},\quad \mathrel{\lor}^{(*)},\quad \mathrel{\longrightarrow}^{(2)},\quad \mathrel{\longleftrightarrow}^{(2)},\] where \(\mathrel{\land}\) and \(\mathrel{\lor}\) have arbitrary arity. This yields the countably infinite set \(\mathcal{Q}\) all quantifier-free formulas. We have countably infinitely many existential and universal quantifiers \[\exists z^{(1)},\quad \forall z^{(1)}\quad \text{for}\quad z \in \mathcal{V}.\] Prenex first-order formulas are built inductively, starting with quantifier-free formulas and applying existential and universal quantifiers. This yields the countably infinite set \(\mathcal{F}\) of all prenex first-order formulas.
We say that a variable \(z \in \mathcal{V}\) occurs in a formula \(\varphi \in \mathcal{F}\) if it appears in an atom of \(\varphi\). If \(z\) additionally occurs in a quantifier in \(\varphi\), we say that \(z\) is a bound variable of \(\varphi\), otherwise \(z\) is a free variable of \(\varphi\). Let \(n \in \mathbb{N}\) and \(z_1\), …, \(z_n \in \mathcal{V}\) with \(z_1 \prec \dots \prec z_n\), and set \(\mathbf{z}= (z_1, \dots, z_n)\). We write \(\mathcal{A}_\mathbf{z}\subseteq \mathcal{A}\) and \(\mathcal{Q}_\mathbf{z}\subseteq \mathcal{Q}\) for the set of all atoms and quantifier-free formulas over variables in \(\mathbf{z}\), respectively. We write \(\mathcal{F}_\mathbf{z}\subseteq \mathcal{F}\) for the set of all those first-order formulas \(\varphi\) for which \(\mathbf{z}\) covers at least the free variables of \(\varphi\). A prenex sentence is a prenex first-order formula \(\vartheta \in \mathcal{F}\) without free variables; \(\mathcal{F}_{()}\) is the set of all sentences.
Consider \(\varphi \in \mathcal{F}\), and let \(\{z_1, \dots, z_n\} \subseteq \mathcal{V}\) be a superset of the free variables of \(\varphi\). Then \(\varphi(z_1, \dots, z_n)\) is called an extended formula. Each extended formula \(\varphi(\mathbf{z})\) induces an interpretation \(\varphi(\mathbf{z})^*: \mathbb{C}^n \to \{0, 1\}\), which is the characteristic function of a relation, inductively defined for \(\mathbf{c}\in \mathbb{C}^n\) as follows:
\((t_1 = t_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(t_1(\mathbf{z})^*(\mathbf{c}) = t_2(\mathbf{z})^*(\mathbf{c})\),
\((t_1 \neq t_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(t_1(\mathbf{z})^*(\mathbf{c}) \neq t_2(\mathbf{z})^*(\mathbf{c})\),
\((t_1 < t_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(t_1(\mathbf{z})^*(\mathbf{c}) < t_2(\mathbf{z})^*(\mathbf{c})\), where \(t_1(\mathbf{z})^*(\mathbf{c})\), \({t_2(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}}\),
\((t_1 \leq t_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(t_1(\mathbf{z})^*(\mathbf{c}) \leq t_2(\mathbf{z})^*(\mathbf{c})\), where \(t_1(\mathbf{z})^*(\mathbf{c})\), \({t_2(\mathbf{z})^*(\mathbf{c}) \in \mathbb{R}}\),
\(\top(\mathbf{z})^*(\mathbf{c}) = 1\),
\(\bot(\mathbf{z})^*(\mathbf{c}) = 0\),
\((\lnot\varphi)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(\varphi(\mathbf{z})^*(\mathbf{c}) = 0\),
\((\varphi_1 \mathrel{\land}\dots \mathrel{\land}\varphi_m)(\mathbf{z})^*(\mathbf{c}) = \min \{\varphi_1(\mathbf{z})^*(\mathbf{c}), \dots, \varphi_m(\mathbf{z})^*(\mathbf{c})\}\),
\((\varphi_1 \mathrel{\lor}\dots \mathrel{\lor}\varphi_m)(\mathbf{z})^*(\mathbf{c}) = \max \{\varphi_1(\mathbf{z})^*(\mathbf{c}), \dots, \varphi_m(\mathbf{z})^*(\mathbf{c})\}\),
\((\varphi_1 \mathrel{\longrightarrow}\varphi_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(\varphi_1(\mathbf{z})^*(\mathbf{c}) \leq \varphi_2(\mathbf{z})^*(\mathbf{c})\),
\((\varphi_1 \mathrel{\longleftrightarrow}\varphi_2)(\mathbf{z})^*(\mathbf{c}) = 1\) iff \(\varphi_1(\mathbf{z})^*(\mathbf{c}) = \varphi_2(\mathbf{z})^*(\mathbf{c})\),
\(\exists z(\varphi)(\mathbf{z})^*(\mathbf{c}) = \max \{\,\varphi(\mathbf{z}, z)^*(\mathbf{c}, c) \mid c \in \mathbb{C}\,\}\), where w.l.o.g. \(z \notin \{z_1, \dots, z_n\}\),
\(\forall z(\varphi)(\mathbf{z})^*(\mathbf{c}) = \min \{\,\varphi(\mathbf{z}, z)^*(\mathbf{c}, c) \mid c \in \mathbb{C}\,\}\), where w.l.o.g. \(z \notin \{z_1, \dots, z_n\}\).
If \(\varphi(\mathbf{z})^*(\mathbf{c}) = 1\) for specific \(\mathbf{c}\in \mathbb{C}^n\), we write \(\mathbb{C}\models \varphi(\mathbf{c})\), where the extension \(\mathbf{z}\) will be clear from the context. If \(\varphi(\mathbf{z})^*(\mathbf{c}) = 1\) for all \(\mathbf{c}\in \mathbb{C}^n\), we call \(\varphi\) a valid formula and write \(\mathbb{C}\models \varphi\), which does not depend on the extension \(\mathbf{z}\); compare Remark 1. According to our definition in the previous section, two terms are equivalent, \(t_1 \approx t_2\), if and only if \(\mathbb{C}\models t_1 = t_2\). We say that two formulas \(\varphi_1\) and \(\varphi_2\) are equivalent if \(\mathbb{C}\models \varphi_1 \mathrel{\longleftrightarrow}\varphi_2\).
We call \(\mathcal{N}_\mathbf{z}\subseteq \mathcal{F}_\mathbf{z}\) a system of normal forms for \(\mathcal{F}_\mathbf{z}\) if for each \(\varphi \in \mathcal{F}_\mathbf{z}\) there is \(\varphi' \in \mathcal{N}_\mathbf{z}\) with \(\mathbb{C}\models \varphi' \mathrel{\longleftrightarrow}\varphi\); we denote \(\varphi'\) by \(\mathcal{N}_\mathbf{z}(\varphi)\). A first-order formula \(\varphi \in \mathcal{F}_\mathbf{z}\) is called a real formula if both sides of all its atoms are real terms.
Proposition 4 (Real normal form of formulas). Consider \(\mathcal{F}_\mathbf{z}\) with \(\mathbf{z}\in \mathcal{V}^n\) for \(n \in \mathbb{N}\). Let \(\mathcal{N}^{(\mathbb{R})}_\mathbf{z}\) be the set of all formulas \(\varphi \in \mathcal{F}_\mathbf{z}\) with the following properties:
all left-hand sides of atoms in \(\varphi\) are polynomials in \(\mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\);
all right-hand sides of atoms in \(\varphi\) are \(0\).
Then \(\mathcal{N}^{(\mathbb{R})}_\mathbf{z}\) is a system of normal forms for \(\mathcal{F}_\mathbf{z}\), and all normal forms in \(\mathcal{N}^{(\mathbb{R})}_\mathbf{z}\) are real formulas.
Proof. Let \(\varphi \in \mathcal{F}_\mathbf{z}\). We transform \(\varphi\) in three subsequent steps as follows:
Equivalently transform all left-hand side and right-hand side terms of atoms in \(\varphi\) into Cartesian normal form according to Proposition 2. Note that within inequalities \(r_1 \leq r_2\) and \(r_1 < r_2\), where \(r_1\), \(r_2\) are real terms, we obtain normal forms in \(\mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\). This yields \(\varphi'\) with \(\mathbb{C}\models \varphi' \mathrel{\longleftrightarrow}\varphi\).
Equivalently rewrite all atoms in \(\varphi'\) as follows, preserving Cartesian normal form: \[f_1 + i \cdot g_1 \mathrel{\rho} f_2 + \mathord{\mathrm{i}}\cdot g_2 \to (f_1 - f_2) + \mathord{\mathrm{i}}\cdot (g_1 - g_2) \mathrel{\rho} 0,\quad \rho \in \{=, \neq, \leq, <\}.\] This yields \(\varphi''\) with \(\mathbb{C}\models \varphi'' \mathrel{\longleftrightarrow}\varphi\). All right-hand sides of atoms in \(\varphi''\) are \(0\), and all left-hand sides of inequalities in \(\varphi''\) are still polynomials in \(\mathbb{Q}[\Re(\mathbf{z}), \Im(\mathbf{z})]\).
Equivalently rewrite equations and disequalities in \(\varphi''\) as follows: \[f + \mathord{\mathrm{i}}\cdot g = 0 \to {f = 0} \mathrel{\mathrel{\land}} {g = 0},\quad f + \mathord{\mathrm{i}}\cdot g \neq 0 \to {f \neq 0} \mathrel{\lor}{g \neq 0}.\] This yields \(\varphi'''\) with \(\mathbb{C}\models \varphi''' \mathrel{\longleftrightarrow}\varphi\), and \(\varphi'''\) has the properties (i) and (ii) specified in the lemma.
◻
4 Quantifier Elimination, Completeness, and Decidability↩︎
Theorem 1 (Pseudo-complex quantifier elimination). Let \(\varphi \in \mathcal{F}_\mathbf{z}\) and assume without loss of generality that \(\varphi\) is in real normal form. Apply the following three steps to compute from \(\varphi\) a quantifier free formula \(\varphi' \in \mathcal{Q}_\mathbf{z}\).
Purification. Replace all subterms \(\Re(z_i)\) and \(\Im(z_i)\) in \(\varphi\) with auxiliary variables \(z^\Re_i\) and \(z^\Im_i\), respectively. Furthermore, replace all quantifiers \(\exists z_i\) and \(\forall z_i\) in \(\varphi\) with \(\exists z^\Re_i\exists z^\Im_i\) and \(\forall z^\Re_i\forall z^\Im_i\), respectively. This yields a first-order formula \(\psi\) in the language of ordered rings.
Real quantifier elimination. Apply any real qe procedure to obtain a quantifier-free formula \(\psi'\) in the language of ordered rings such that \(\mathbb{R}\models \psi \mathrel{\longleftrightarrow}\psi'\).
Substitution. Remove the auxiliary variables via substitution of the original terms. This yields \(\varphi' \in \mathcal{Q}_\mathbf{z}\) where \(\varphi' = \psi'[z^\Re_i \gets \Re(z_i), z^\Im_i \gets \Im(z_i)]\).
Then \(\mathbb{C}\models \varphi \mathrel{\longleftrightarrow}\varphi'\). In other words, our three steps establish a quantifier elimination procedure for the complex numbers in our language \(\mathcal{L}\).
Proof. Consider extended formulas \(\varphi(\mathbf{z})\), \(\varphi'(\mathbf{z})\) and \(\psi(\mathbf{z}^\Re, \mathbf{z}^\Im)\), \(\psi'(\mathbf{z}^\Re, \mathbf{z}^\Im)\), and their interpretations \[\varphi(\mathbf{z})^*, \varphi'(\mathbf{z})^*: \mathbb{C}^n \to \{0, 1\},\quad \psi(\mathbf{z}^\Re, \mathbf{z}^\Im)^*, \psi'(\mathbf{z}^\Re, \mathbf{z}^\Im)^*: \mathbb{R}^{2n} \to \{0, 1\}.\]
As an auxiliary lemma, we prove by strong induction on the number \(q\) of prenex quantifiers in \(\varphi\) that \[\label{EQ:th1claim} \varphi(\mathbf{z})^*(\mathbf{c}) = \psi(\mathbf{z}^\Re, \mathbf{z}^\Im)^*(\Re^*(\mathbf{c}), \Im^*(\mathbf{c}))\quad \text{for all}\quad \mathbf{c}\in \mathbb{C}^n.\tag{1}\] For \(q=0\), the claim 1 is immediate. Assume \(q > 0\) and let \(\mathbf{c}\in \mathbb{C}^n\). Assume without loss of generality that \(\varphi = (\exists z \tilde{\varphi})\) and \(\psi = (\exists z^\Re\exists z^\Im\tilde{\psi})\) with extended formulas \(\tilde{\varphi}(z, \mathbf{z})\) and \(\tilde{\psi}(z^\Re, \mathbf{z}^\Re, z^\Im, \mathbf{z}^\Im)\) and corresponding interpretations on \(\mathbb{C}^{n+1}\) and \(\mathbb{R}^{2n+2}\), respectively. By the induction hypothesis we have \[\label{EQ:Th1ih} \tilde{\varphi}(z, \mathbf{z})^*(c, \mathbf{c}) = \tilde{\psi}(z^\Re, \mathbf{z}^\Re, z^\Im, \mathbf{z}^\Im)^*(\Re^*(c), \Re^*(\mathbf{c}), \Im^*(c), \Im^*(\mathbf{c})).\tag{2}\] Combining 2 with the formal semantics of quantifiers (see the enumeration on p. ), we obtain \[\begin{align} \label{EQ:minmax} (\exists z \tilde{\varphi})(\mathbf{z})^*(\mathbf{c}) & = \max_{c \in \mathbb{C}}\bigl(\tilde{\varphi}(z,\mathbf{z})^*(c,\mathbf{c})\bigr)\notag\\ & = \max_{c\in \mathbb{C}}\bigl( \tilde{\psi}( z^\Re, \mathbf{z}^\Re, z^\Im, \mathbf{z}^\Im)^*(\Re^*(c), \Re^*(\mathbf{c}), \Im^*(c), \Im^*(\mathbf{c}))\bigr)\notag\\ & = \max_{r_1, r_2 \in \mathbb{R}}\bigl( \tilde{\psi}( z^\Re, \mathbf{z}^\Re, z^\Im, \mathbf{z}^\Im)^*(r_1, \Re^*(\mathbf{c}), r_2, \Im^*(\mathbf{c}))\bigr)\notag\\ &= (\exists z^\Re\exists z^\Im\tilde{\psi})(\mathbf{z}^\Re, \mathbf{z}^\Im)^*(\Re^*(\mathbf{c}), \Im^*(\mathbf{c})). \end{align}\tag{3}\] With universal quantifiers \(\varphi = (\forall z \tilde{\varphi})\) and \(\psi = (\forall z^\Re\exists z^\Im\tilde{\psi})\) the same argument holds with \(\min\) instead of \(\max\) in 3 . This proves our auxiliary lemma 1 . Hence, \[\begin{align} \varphi(\mathbf{z})^*(\mathbf{c}) & = \psi(\mathbf{z}^\Re, \mathbf{z}^\Im)^*(\Re^*(\mathbf{c}), \Im^*(\mathbf{c})) & & \text{purification, using \eqref{EQ:th1claim}}\\ & = \psi'(\mathbf{z}^\Re, \mathbf{z}^\Im)^*(\Re^*(\mathbf{c}), \Im^*(\mathbf{c})) & & \text{real \mathrm{\small qe}}\\ & = \varphi'(\mathbf{z})^*(\mathbf{c}) & & \text{substitution} \end{align}\] for all \(\mathbf{c}\in \mathbb{C}^n\). ◻
Corollary 1 (Completeness and decidability). The theory \(\Theta = \{\,\vartheta \in \mathcal{F}_{()} \mid \mathbb{C}\models \vartheta\,\}\) is complete and decidable. Our pseudo-complex quantifier elimination procedure yields a decision procedure for \(\Theta\).
Proof. When applying the qe procedure in the proof of Theorem 1 to a sentence \(\vartheta \in \mathcal{F}_{()}\), the purified formula \(\psi\) is a sentence, too. Modulo obvious simplifications, real qe applied to \(\psi\) will yield either \(\top\) or \(\bot\), which is preserved by the subsequent substitution step. In the former case, \(\mathbb{C}\models \vartheta \mathrel{\longleftrightarrow}\top\) and thus \(\vartheta \in \Theta\); else \(\mathbb{C}\models \vartheta \mathrel{\longleftrightarrow}\bot\), equivalently \(\mathbb{C}\models \lnot\vartheta \mathrel{\longleftrightarrow}\top\), and thus \(\vartheta \notin \Theta\) and \(\lnot\vartheta \in \Theta\). ◻
5 Complex Reinterpretation↩︎
We present a method for simplifying the output formula of our quantifier elimination procedure by combining real atoms of the form \(r_1 = 0 \mathrel{\land}r_2 = 0\) into a single atom \(r_1 + \mathord{\mathrm{i}}\cdot r_2 = 0\). Subsequent conversion of all terms into conjugate normal form can result in a more compact formula. In the special case \(\Re(z) = 0 \mathrel{\land}\Im(z) = 0\), the resulting terms even collapse to a single variable, yielding \(z = 0\).
For our presentation here we assume without loss of generality that the input formula of our method is a conjunction of real atoms, and we focus on equations. It is easy to see that a dual variant with disjunctions and disequalities exists.1 Note that ordering inequalities cannot be straightforwardly combined, as they are equivalent to \(\bot\) in the presence of non-real terms. Moreover, disequalities cannot be directly combined within a conjunction.
We are thus given a set \(R = \{r_1 = 0, \ldots, r_n = 0\}\) of equations, where each \(r_i\) is a real term, and our goal is to find a pairing of elements of \(R\) that minimizes the total size of the resulting merged equations together with the remaining unpaired equations. This can be viewed as a variant of the minimum edge cover problem in the following sense.
Definition 1 (Minimum cost partial edge cover). Let \(G = (V, E)\) be an undirected graph, \(c_V \colon V \to \mathbb{N}\) a cost function on the vertices, and \(c_E \colon E \to \mathbb{N}\) a cost function on the edges. For any subset \(S \subseteq E\), we denote by \(V(S) \subseteq V\) the set of all endpoints of edges in \(S\). A minimum cost partial edge cover (mcpec) is a subset \(S \subseteq E\) that minimizes \(c(S) = \sum_{v \in V \setminus V(S)} c_V(v) + \sum_{e \in S} c_E(e)\).
We fix a system of normal forms \(\mathcal{N}_\mathbf{z}\) for atomic formulas \(\mathcal{A}_\mathbf{z}\) and denote by \(|\alpha|\) the word length of \(\alpha \in \mathcal{A}_\mathbf{z}\). We choose \(V = R\) with a cost function \(c_V(r_i = 0) = |\mathcal{N}_\mathbf{z}(r_i = 0)|\), and \(E = \{\,\{v, w\} \mid v, w \in V, v \neq w\,\}\) with a cost function \[\label{EQ:minimize} c_E(\{r_i = 0, r_j = 0\}) = \min \{ |\mathcal{N}(r_i + \mathord{\mathrm{i}}\cdot r_j = 0)|, |\mathcal{N}(r_j + \mathord{\mathrm{i}}\cdot r_i = 0)| \}.\tag{4}\] For any edge \(e \in E\), we denote by \(\mu(e)\) the equation that minimizes 4 . The following proposition shows how to use a solution \(S \subseteq E\) of the mcpec problem to construct a formula that is equivalent to \(\bigwedge R\).
Proposition 5. Let \(G = (V, E)\) be the graph constructed from a set of equations \(R\) and let \(S \subseteq E\). Then \(\mathbb{C}\models \bigwedge R \mathrel{\longleftrightarrow}\bigwedge \bigl(V \setminus V(S)\bigr) \mathrel{\land}\bigwedge_{e \in S} \mu(e)\).
Proof. If an equation \(r_i = 0\) is covered by multiple edges in \(S\), we use idempotence to replace it with \(r_i = 0 \mathrel{\land}\dots \mathrel{\land}r_i = 0\) on the left-hand side of the equivalence. Then the statement follows directly since \(\mathbb{C}\models r_i = 0 \mathrel{\land}r_j = 0 \mathrel{\longleftrightarrow}\mu(e)\) for all \(\{r_i = 0, r_j = 0\} \in S\) by construction. ◻
Example 2. Fix a system of normal forms \(\mathcal{N}_\mathbf{z}\) of \(\mathcal{A}_\mathbf{z}\) such that all atoms are of the form \(t \mathrel{\rho} 0\) where either \(t = 0\) or \(t \in \mathbb{Q}[\mathord{\mathrm{i}}][\mathbf{z},\overline{\mathbf{z}}]\) with leading coefficient \(1\). Consider the formula \[\label{EQ:exmcpecin} \Re(x) = 0 \mathrel{\land}\Im(x) = 0 \mathrel{\land}\Re(y) = 0 \mathrel{\land}\Im(y) > 0.\tag{5}\]
We have \((V, E)\) with costs \(c_V\), \(c_E\) as follows:
Figure 1: 
.
For instance, \(c_V(\Re(x) = 0) = |x + \overline{x} = 0| = 6\) and \[c_E(\{\Re(x) = 0, \Im(x) = 0\}) = \min \{ |x = 0|, |\overline{x} = 0| \} = 3.\] The mcpec is given by \(S = \bigl\{\{\Re(x) = 0, \Im(x) = 0\}\bigr\}\) corresponding to the merged equation \(x = 0\) with cost \(3\), and the remaining unpaired equation \(\Re(y) = 0\) with cost \(6\). This yields the following equivalent of 5 : \[x = 0 \mathrel{\land}y + \overline{y} = 0 \mathrel{\land}\mathord{\mathrm{i}}\overline{y} - \mathord{\mathrm{i}}y > 0.\]
The mcpec problem can be efficiently solved using ideas from combinatorial optimization, specifically reduction to the maximum weight matching problem [23]. We denote by \(E(v)\) the set of all edges incident to a vertex \(v \in V\). A subset \(M \subseteq E\) is a matching if no two edges in \(M\) share a common endpoint. A maximum weight matching is a matching \(M\) that maximizes \(c_E(M) = \sum_{e \in M} c_E(e)\).
Lemma 1 (Complexity of the mcpec problem with low vertex costs). Consider an instance of the mcpec problem for a graph \(G = (V, E)\) with cost functions \(c_V\) and \(c_E\). Assume that for all vertices \(v \in V\) and edges \(e \in E(v)\), the cost functions satisfy \(c_V(v) \leq c_E(e)\). Then an mcpec can be computed in time \(O(n \cdot (m + n \log n))\), where \(n = |V|\) and \(m = |E|\) are the numbers of vertices and edges in \(G\), respectively.
Proof. We construct a new graph \(G' = (V', E')\) with cost function \(c' \colon E' \to \mathbb{Z}\) as follows. Set \(V' = V\), \(E' = E\), and for each edge \(e \in E\) with endpoints \(v\) and \(w\), define \(c'(e) = c_V(v) + c_V(w) - c_E(e)\). We claim that every maximum weight matching \(M \subseteq E\) in \(G'\) is an mcpec in \(G\) and can thus be computed in time \(O\bigl(n \cdot (m + n \log n)\bigr)\) [24].
To prove the claim, we first consider a partial edge cover \(S \subseteq E\) in \(G\) and show that it can be transformed into a matching without increasing its partial edge cover cost in \(G\). Assume \(S\) is not a matching. Then there exist two edges \(e_1\), \(e_2 \in S\) that share a common endpoint \(v \in V\). Denote by \(w\) the other endpoint of \(e_1\). Since \(c_V(w) \leq c_E(e_1)\) by assumption, we can remove \(e_1\) from \(S\) while not increasing the total cost of \(S\). Repeating this process until no two edges in \(S\) share a common endpoint results in a matching.
We come back to our initial claim that every maximum weight matching \(M\) in \(G'\) is an mcpec in \(G\). Assume for a contradiction that there exists a partial edge cover \(S\) in \(G\) with \(c(S) < c(M)\). By the first part of our proof, we can assume without loss of generality that \(S\) is a matching. Therefore, we have \[\begin{align} c(S) &= \sum_{v \in V \setminus V(S)} c_V(v) + \sum_{e \in S} c_E(e) = \sum_{v \in V} c_V(v) - \sum_{v \in V(S)} c_V(v) + \sum_{e \in S} c_E(e) \\ &= \sum_{v \in V} c_V(v) - \sum_{e \in S} c'(e) = \sum_{v \in V} c_V(v) - c'(S) \end{align}\] and, similarly, \(c(M) = \sum_{v \in V} c_V(v) - c'(M)\). Since \(c(S) < c(M)\), this implies \(c'(S) > c'(M)\), which contradicts the assumption that \(M\) is a maximum weight matching in \(G'\). ◻
We finally show that complexity of the mcpec problem in the general case can be reduced to the special case considered in the previous lemma.
Proposition 6 (Complexity of the mcpec problem). The mcpec problem for a graph \(G = (V, E)\) with cost functions \(c_V\) and \(c_E\) can be solved in time \(O\bigl(n \cdot (m + n \log n)\bigr)\), where \(n = |V|\) and \(m = |E|\) are the number of vertices and edges in \(G\).
Proof. We construct a new graph \(G' = (V', E')\) with \(V' = V\), \(E' = E\), \(c_E' = c_E\), and a new vertex cost function \(c_V' \colon V' \to \mathbb{N}\), \(c_V'(v) = \min \{ c_V(v), c_E(e_v) \}\), where \(e_v \in E\) is an edge with minimum cost among all edges with endpoint \(v\). By construction, \(G'\) satisfies the assumptions of the previous lemma, and an mcpec\(S'\) in \(G'\) can be computed in time \(O\bigl(n \cdot (m + n \log n)\bigr)\). Our final mcpec in \(G\) is then given \(S = S' \cup S''\) with \(S'' = \{ e_v \mid v \in V \setminus V(S'), \, c_E(e_v) < c_V(v) \}\). It remains to show that \(S\) is indeed an mcpec in \(G\). First, note that \(S'\) and \(S''\) are disjoint, so that \[c(S) = \sum_{v \in V \setminus V(S)} c_V(v) + \sum_{e \in S'} c_E(e) + \sum_{e \in S''} c_E(e).\] By definition of \(S''\) and \(c_V'\), we have \(S'' \subseteq V \setminus V(S') \cap V(S'')\) and \[\sum_{e \in S''} c_E(e) = \sum_{e_v \in S''} c_V'(v) \leq \sum_{v \in V \setminus V(S') \cap V(S'')} c'_V(v).\] Moreover, \(V \setminus V(S) = V \setminus V(S') \cap V \setminus V(S'')\) and \(c_V(v) = c_V'(v)\) for all \(v \in V \setminus V(S)\) by the definition of \(S''\) and \(c_V'\). Therefore, \[\sum_{v \in V \setminus V(S)} c_V(v) = \sum_{v \in V \setminus V(S') \cap V \setminus V(S'')} c'_V(v).\] By combining the previous equation and inequality, we obtain \[\sum_{v \in V \setminus V(S)} c_V(v) + \sum_{e \in S''} c_E(e) \leq \sum_{v \in V \setminus V(S')} c'_V(v).\] Using \(c'_E = c_E\), we conclude that \(c(S) \leq c'(S')\). Since \(S'\) is an mcpec in \(G'\), and because \(c'(T) \leq c(T)\) for any \(T \subseteq E\) by definition of \(c'\), it follows that \(c(S) \leq c'(S') \leq c'(T) \leq c(T)\) for any partial edge cover \(T\) in \(G\). Hence, \(S\) is an mcpec in \(G\). ◻
6 Complexity↩︎
We summarize the asymptotic complexity of the quantifier elimination problem for the theory \(\textrm{ACF}_0\) of algebraically closed fields of characteristic zero and the theory \(\textrm{RCF}\) of real closed fields. Furthermore, we examine the complexity of available algorithms, with a particular emphasis on well-supported implementations. On this basis, we address some implications for the framework proposed here.
With respect to word length, the asymptotic worst-case size of the qe output in both \(\textrm{ACF}_0\) and \(\textrm{RCF}\) is doubly exponential in the size of the input, and this bound is tight. This yields doubly exponential time complexity [7], [25], [26]. It is noteworthy that elimination procedures for \(\textrm{ACF}_0\) admit exponential-space bounds [27], and the corresponding qe algorithms can be implemented within exponential space provided the output is generated incrementally. When the number of alternations between existential and universal quantifiers in the input is bounded, the time complexity for both \(\textrm{ACF}_0\) and \(\textrm{RCF}\) is singly exponential [28], [29]. The complexity depends primarily on the number of quantifier alternations and the number of quantified variables, which determine the exponent in the standard bounds for qe in \(\textrm{ACF}_0\) [28] and \(\textrm{RCF}\) [29]–[31]. Asymptotically, these bounds have the same form for \(\textrm{ACF}_0\) and \(\textrm{RCF}\).
Remark 2 (Asymptotic complexity of pseudo-complex qe). Asymptotic complexity bounds for real qe carry over to pseudo-complex qe. During the purification step in Theorem 1, the input size for real qe may grow polynomially in the original input size. More specifically, the number of quantifiers in the input doubles, while the number of quantifier alternations remains unchanged. Subsequent complex reinterpretation of the qe result is polynomial in the size of the result and thus dominated by the complexity bounds for qe.0◻
From a practical perspective, qe in \(\textrm{ACF}_0\) can be approached via comprehensive Gröbner bases (cgb) [16]. The Redlog system [15] implements this by computing disjunctive normal forms at each quantifier alternation and employing cgb computations with disjoint case distinctions on parameter vanishing, which leads to extremely rapid growth of the resulting quantifier-free formulas. Compared to \(\textrm{ACF}_0\), qe in \(\textrm{RCF}\) is supported more extensively across a wide range of software environments, including systems such as Qepcad, Redlog, Maple, and Mathematica. Numerous applications in the sciences and engineering are documented in the literature; see e.g. [11], [20] and the references therein. For general-purpose applications, the method of choice remains partial cylindrical algebraic decomposition [6]. This algorithm has doubly exponential complexity in the total number of variables occurring in the input, regardless of the presence of quantifier alternations or even whether a variable is quantified [32].
On the one hand, the strong available software support for real qe facilitates the integration of our approach into the corresponding software environments. On the other hand, the lack of efficient implementations of complex qe suggests that our method may be of interest even for complex qe problems without our additional operations.
7 Implementation and Examples↩︎
We have implemented our approach in our Python-based open-source system Logic1.2 For the real qe part, Logic1 uses by default an implementation of virtual substitution following essentially [9]. Note, that real qe serves as a black box so that it is not hard to plug in alternative implementations in the future. An interface to Redlog [15] already exists. Our implementation allows to dynamically switch between conjugate and Cartesian normal forms.
The computation times for all subsequent examples are summarized in Table 2 on p., which also indicates which of the two available normal forms for terms was chosen in each case.
Example 3 (Cartesian coordinates). The representation of a complex number \(z\) in Cartesian coordinates can be expressed by the following formula: \[\varphi = \forall z \exists x \exists y \bigl(\Im(x) = 0 \mathrel{\land}\Im(y) = 0 \mathrel{\land}z = x + \mathord{\mathrm{i}}\cdot y\bigr).\] Quantifier elimination yields the quantifier-free formula \(\top\).
Example 4 (Roots of unity). In contrast to the real numbers, the complex numbers contain a square root of \(-1\). This can be expressed as \(\varphi_1 = \exists z(z^2 + 1 = 0)\), for which quantifier elimination yields the quantifier-free formula \(\top\). More generally, Weispfenning discusses the equivalence of the following formula to \(d^4 - 1 = 0\) as an example for complex qe using comprehensive Gröbner bases [16]: \[\varphi_2 = \exists c \forall b \forall a \bigl((a = d \mathrel{\land}b = c) \mathrel{\lor}(a = c \mathrel{\land}b = 1) \mathrel{\longrightarrow}b = a^2 \bigr).\] Our qe applied to \(\varphi_2\) yields \(d + 1 = 0 \mathrel{\lor}d + i = 0 \mathrel{\lor}d - 1 = 0 \mathrel{\lor}d - i = 0\), corresponding to the factorization of \(d^4 - 1\) over \(\mathbb{C}\).
Example 5 (Counterexample for geometry provers). In his famous monograph [33], Chou presents the following example of a formula that holds over \(\mathbb{R}\) but not over \(\mathbb{C}\): \[\varphi = \forall x_{1} \forall x_{2} \bigl(x_{1}^2 + x_{2}^2 = 1 \mathrel{\land}x_{1} = 2 \mathrel{\longrightarrow}x_{2} = 1\bigr).\] Indeed, the unit circle \(x_1^2 + x_2^2 = 1\) does not intersect with the line \(x_1 = 2\), hence the left side of the implication is equivalent to \(\bot\). Our qe yields the quantifier-free formula \(\bot\) over \(\mathbb{C}\).
Hilbert spaces generalize the Euclidean space \(\mathbb{R}^n\) to a more abstract setting where there still exists a notion of angles, captured via an inner product. They are fundamental in science and engineering, particularly in the formulation of quantum mechanics [34] as well as in various applications in signal processing [35] and machine learning [36]. We consider the Hilbert space \(\mathbb{C}^n\) with an inner product \(\langle \cdot, \cdot \rangle: \mathbb{C}^n \times \mathbb{C}^n \to \mathbb{C}\) defined by \[\langle \mathbf{v}, \mathbf{w}\rangle = \sum_{i=1}^n v_i \cdot \overline{w_i}\] for all \(\mathbf{v}= (v_1, \dots, v_n) \in \mathbb{C}^n\) and \(\mathbf{w}= (w_1, \dots, w_n) \in \mathbb{C}^n\).
Example 6 (Orthogonality). Two vectors \(\mathbf{v}, \mathbf{w}\in \mathbb{C}^n\) are called orthogonal if \(\langle \mathbf{v}, \mathbf{w}\rangle = 0\). Consider the following formula with free variables \(v_1\), …, \(v_n\): \[\varphi = \forall w_1 \dots \forall w_n \bigl(\langle \mathbf{v}, \mathbf{w}\rangle = 0\bigr).\] We obtain the quantifier-free formula \(v_1 = 0 \mathrel{\land}v_2 = 0 \mathrel{\land}v_3 = 0\) for \(n = 3\). This proves a special case of the more general fact that \(\mathbf{v}\in \mathbb{C}^n\) is zero if and only if it is orthogonal to all vectors in \(\mathbb{C}^n\). Table 1 summarizes computation times for growing values of \(n\).
| \(n\) | ||||||||
|---|---|---|---|---|---|---|---|---|
| time (s) |
Example 7 (Cauchy–Schwarz inequality). The Cauchy–Schwarz inequality is fundamental in linear algebra and functional analysis. It can be expressed by the following formula with free variables \(v_1\), …, \(v_n\): \[\varphi = \forall w_1 \dots \forall w_n \bigl(\langle \mathbf{v}, \mathbf{w}\rangle \cdot \overline{\langle \mathbf{v}, \mathbf{w}\rangle} \leq \langle \mathbf{v}, \mathbf{v}\rangle \cdot \langle \mathbf{w}, \mathbf{w}\rangle\bigr),\] where \(\langle \mathbf{v}, \mathbf{w}\rangle \cdot \overline{\langle \mathbf{v}, \mathbf{w}\rangle} = |\langle \mathbf{v}, \mathbf{w}\rangle|^2\). We obtain the quantifier-free formula \(\top\) for \(n\) from \(1\) to \(4\).
In quantum mechanics, the state of a physical system is represented by a vector in a complex Hilbert space \(H\), and physical observables correspond to self-adjoint linear operators \(A \colon H \to H\). The expected value of the measurement outcome of an observable \(A\) on a state \(\mathbf{v}\in H\) is \(\langle A \mathbf{v}, \mathbf{v}\rangle\). In the special case of a single qubit, the state space is given by \(H = \mathbb{C}^2\).
Example 8 (Self-adjoint matrices). Consider a matrix \(A = (a_{ij})_{i,j=1}^n \in \mathbb{C}^{n \times n}\). Then \(A\) is self-adjoint if and only if \[\varphi_1 = \forall v_1 \dots \forall v_n \forall w_1 \dots \forall w_n \bigl(\langle A \mathbf{v}, \mathbf{w}\rangle = \langle \mathbf{v}, A \mathbf{w}\rangle\bigr).\] Applying qe in the case of a single qubit, i.e. \(n = 2\), we obtain the equivalent quantifier-free formula \(a_{11} - \overline{a_{11}} = 0 \mathrel{\land}a_{12} - \overline{a_{21}} = 0 \mathrel{\land}a_{22} - \overline{a_{22}} = 0\). This is a special case of the well-known characterization of self-adjoint matrices as those that are equal to their conjugate transpose, i.e. \(a_{ij} = \overline{a_{ji}}\) for all \(i\), \(j \in \{1, \dots, n\}\). Alternatively, self-adjointness can be characterized by the following formula: \[\varphi_2 = \forall v_1 \dots \forall v_n \bigl(\Im(\langle A \mathbf{v}, \mathbf{v}\rangle) = 0\bigr).\] Applying qe again in the case \(n = 2\), we obtain the same quantifier-free equivalent as above. In particular, this shows that the expected measurement outcome of a quantum observable \(A\) on a single qubit is always real, i.e. physically meaningful.
Example 9 (Density matrices). A probabilistic mixture of states of a quantum system can be represented by a density matrix, which is a self-adjoined, positive semidefinite matrix with trace \(1\). In the case of a single qubit, a self-adjoined matrix \(A \in \mathbb{C}^{2 \times 2}\) with trace \(1\) has the form \[A = \begin{pmatrix} \Re(a) & b\\ \overline{b} & 1 - \Re(a) \end{pmatrix} \quad \text{for a, b \in \mathbb{C}}.\] The positive semidefiniteness of \(A\) can be expressed by the following formula: \[\varphi = \forall v_1 \forall v_2 \bigl(\langle A \mathbf{v}, \mathbf{v}\rangle \geq 0\bigr).\] Note that \(\langle A \mathbf{v}, \mathbf{v}\rangle \in \mathbb{R}\) for all \(\mathbf{v}\in \mathbb{C}^2\), which can be proved using a normal form computation. Applying qe, we obtain the following quantifier-free formula: \[\begin{gather} \Re(a) \geq 0 \mathrel{\land}\bigl(\Re(a) = 0 \mathrel{\lor}\Re(a)^{2} + \Re(\mathit{b})^{2} + \Im(b)^{2} - \Re(a) \leq 0\bigr) \\ {}\mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Re(b) = 0\bigr) \mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Re(b) \leq 0\bigr) \mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Re(b) \geq 0\bigr)\\ {}\mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Im(b) = 0 \mathrel{\lor}\Re(b)^{2} \Im(b) + \Im(b)^{3} \leq 0\bigr)\\ {}\mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Im(b) = 0 \mathrel{\lor}\Re(b)^{2} \Im(b) + \Im(b)^{3} \geq 0\bigr)\\ {}\mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Im(b) \leq 0\bigr) \mathrel{\land}\bigl(\Re(a) > 0 \mathrel{\lor}\Im(b) \geq 0\bigr). \end{gather}\] This can be further simplified by hand to \(\Re(b)^{2} + \Im(b)^{2} \leq \Re(a) \cdot (1 - \Re(a))\).
Another important application of complex numbers in science and engineering is in the analysis of electrical circuits [37]. A special class of such circuits are \(RC\) filters, which are designed to allow signals of certain frequencies to pass while damping signals of other frequencies. In the analysis of filters, their transfer function \(H(s) = {p(s)}/{q(s)}\) plays a central role, where \(p(s)\) and \(q(s)\) are polynomials in a complex variable \(s\); see [38].
The qe in our following examples using external assumptions [19]. The input is a first-order formula \(\varphi\) plus a list \(A\) of atoms. The output is a quantifier-free formula \(\varphi'\) such that \(\mathbb{C}\models \bigwedge A \mathrel{\longrightarrow}(\varphi \mathrel{\longleftrightarrow}\varphi')\). Note that this yields \(\mathbb{C}\models \varphi \mathrel{\longleftrightarrow}\varphi'\) as usual when \(A\) is empty.
Example 10 (Gain of passive \(RC\) high-pass filter). Figure 2 shows a circuit diagram of a passive \(RC\) high-pass filter, which consists of a capacitor \(C\) and a resistor \(R\). It has the transfer function \(H(s) = {p(s)}/{q(s)}\) with \(p(s) = R Cs\) and \(q(s) = RCs + 1\). The gain at a frequency \(\omega \in \mathbb{R}\) is given by \(|H(\omega\mathord{\mathrm{i}})|\). The following formula expresses that the gain of the filter is bounded by \(g\) for all frequencies: \[\varphi = \forall s \bigl(\Re(s) = 0 \mathrel{\longrightarrow}p(s)\overline{p(s)} < g^2 \cdot q(s)\overline{q(s)}\bigr),\] where \(p(s)\overline{p(s)} = |p(s)|^2\) and \(q(s)\overline{q(s)} = |q(s)|^2\). Under the assumptions \[A = \{\Re(R) > 0,\, \Im(R) = 0,\, \Re(C) > 0,\, \Im(C) = 0,\, \Re(g) > 0,\, \Im(g) = 0\},\] we obtain the quantifier-free formula \[\Re(g)^2 - 1 \geq 0.\] Recall that there is an assumption \(\Im(g) = 0\) in \(A\).
Example 11 (Stability of active \(RC\) filter). Figure 3 shows a circuit diagram of the active \(RC\) filter from [39]. It consists of resistors \(R_1\), …, \(R_{11}\), capacitors \(C_1\), \(C_2\) and four operational amplifiers. Denote by \(G_i = {1}/{R_i}\) the conductance of resistor \(R_i\). Then the transfer function is given by \(H(s) = {p(s)}/{q(s)}\) with \(p(s)\) and \(q(s)\) as follows: \[\begin{align} p(s) & = -G_4G_8(G_1G_2G_9 + G_1G_3G_9 + G_1G_9G_1 + G_2G_6G_9) \\ & \phantom{=} \quad + G_7C_2(G_1G_3G_9 + G_1G_3G_1) \cdot s - G_2G_7C_1C_2G_9 \cdot s^2, \\ q(s) &= G_1G_9G_4G_6G_8 + G_1G_9G_5G_7G_2 \cdot s + G_1G_9G_7G_1G_2 \cdot s^2. \end{align}\] A circuit is called stable if its transfer function has no poles in the right half-plane. The following formula gives a sufficient condition with free variables \(G_1\), …, \(G_9\), \(C_1\), \(C_2\): \[\varphi = \forall s \bigl(q(s) = 0 \mathrel{\longrightarrow}\Re(s) < 0\bigr).\] Quantifier elimination yields the quantifier-free formula \(\top\) under the physically motivated assumption that all free variables stand for positive real numbers, i.e., \[A = \bigl\{\Re(G_i) > 0,\, \Im(G_i) = 0\bigr\}_{i \in \{1, \dots, 9\}} \cup \bigl\{\Re(C_j) > 0,\, \Im(C_j) = 0\bigr\}_{j \in \{1, 2\}}.\]
![Figure 3: Circuit diagram of an active RC filter; see [39]](/article/2604.26400/_pdflatex/oxfiysuq.png "fig:")
| normal form used | time (s) | ||
|---|---|---|---|
| 3 | Cartesian coordinates | conjugate | 0.04 |
| 4 | Roots of unity, \(\varphi_1\) | conjugate | 0.03 |
| 4 | Roots of unity, \(\varphi_2\) | conjugate | 1.23 |
| 5 | Counterexample for geometry provers | conjugate | 0.07 |
| 6 | Orthogonality (\(n = 3\)) | conjugate | 0.2 |
| 7 | Cauchy-Schwarz inequality (\(n = 4\)) | conjugate | 24.57 |
| 8 | Self-adjoint matrices, \(\varphi_1\) | conjugate | 1.28 |
| 8 | Self-adjoint matrices, \(\varphi_2\) | conjugate | 0.91 |
| 9 | Density matrices | Cartesian | 1.79 |
| 10 | Gain of passive \(RC\) high-pass filter | Cartesian | 2.64 |
| 11 | Stability of active \(RC\) filter | conjugate | 3.76 |
8 Conclusions↩︎
We have introduced a formal logical framework for the complex numbers that includes symbols for the imaginary unit, as well as for real and imaginary parts and complex conjugation. Within this framework, additional operations, such as the complex absolute value, become definable. The corresponding first-order theory is complete and decidable, and it admits effective quantifier elimination. From a technical perspective, our approach builds on quantifier elimination over the real numbers, allowing existing implementations to be used as a black box. Compared with the classical theory of algebraically closed fields of characteristic zero in the language of rings, our framework is often better aligned with the needs of applications in the sciences and engineering. To illustrate its practical utility, we have presented several academic examples computed using an implementation in our Python-based open-source system Logic1.
Acknowledgments↩︎
Nicolas Faroß is currently supported by SSF (Swedish Foundation for Strategic Research), grant number FUS21-0063.
References↩︎
In practice, we employ a simplification framework with implicit theories similar to [22], which is beyond the scope of this article. Simpler implementations could rely on Boolean normal form computations. Our approach smoothly integrates the conjunctive and disjunctive variants while avoiding exponential blow-up.↩︎