Complex

A first-order theory of complex numbers following [FarossSturm-2026].

In this theory, terms are polynomial expressions built from rational numbers, the imaginary unit \(i\), complex variables, complex conjugation, and real and imaginary parts.

To construct Terms, one can obtain Variables from the global variable set VV. These can be combined using arithmetic +, -, *, /, **, the imaginary unit I, and the functions Re, Im, and Conj to build larger terms. The symbol ~ is an alias for Conj.

>>> from logic1.firstorder import *
>>> from logic1.theories.Complex import *
>>> a, b = VV.get('a', 'b')
>>> 2 * a**2 * Conj(b) - 1
2 * a**2 * ~b - 1
>>> (a + I)**2
a**2 + 2 * I * a - 1
>>> Re(a)**2 + Im(a)**2
a * ~a

Note that terms are represented by default in conjugate normal form, i.e. as polynomials in complex variables and their conjugates. This can be changed to cartesian normal form using the function Term.set_normal_form.

>>> z = VV['z']
>>> z * Re(z)
1/2 * z**2 + 1/2 * z * ~z
>>> old_normal_form = Term.set_normal_form(cartesian_normal_form)
>>> z * Re(z)
Re(z)**2 + I * Re(z) * Im(z)
>>> _ = Term.set_normal_form(old_normal_form)

Atomic formulas in this theory of complex numbers are given by equalities and inequalities between terms and can be constructed using the usual comparison operators (==, !=, <, <=, >, >=). However, inequalities are restricted to the case where both sides are real terms.

>>> z = VV['z']
>>> z == 0
z == 0
>>> Re(z) < 0
1/2 * z + 1/2 * ~z < 0
>>> z >= 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z >= 0 because it is not real

Given a Formula in this theory of complex numbers, one can use the functions simplify and qe for simplification and quantifier elimination, respectively.

>>> z = VV['z']
>>> simplify(z**2 * Conj(z) == 0)
z == 0
>>> qe(Ex(z, z**2 + 1 == 0))
T