Decision problems for language equations

Equations with formal languages as unknowns using all Boolean operations and concatenation are studied. Their main properties, such as solution existence and uniqueness, are characterized by first-order formulae. It is shown that testing solution existence is Π1-complete, while solution uniqueness and existence of a least and of a greatest solution are all Π2-complete problems. The families of languages defined by components of unique, least and greatest solutions of such systems are shown to coincide with the classes of recursive, recursively enumerable and co-recursively enumerable sets, respectively.