Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity $\forall\,x\,.\,\Phi \equiv \neg (\exists\,x\,.\,\neg \Phi)$. If $\Phi$ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blow-up. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated by different means without this blow-up by treating them as first-class citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blow-up is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the na\"ive doubly exponential blow-up, perhaps at least in restricted settings. In this paper, we answer this question negatively and show that there is a family of NFA representing automatic relations for which the minimal NFA recognising the language after eliminating a single universal quantifier is doubly exponential, and deciding whether this language is empty is ExpSpace-complete.

翻译：自动结构是一种宇宙和关系均可表示为正则语言的结构。根据正则语言的标准闭包性质，自动结构的一阶理论是可判定的。虽然存在量词可以通过同态应用在线性时间内消去，但全称量词通常通过恒等式 $\forall\,x\,.\,\Phi \equiv \neg (\exists\,x\,.\,\neg \Phi)$ 消去。若 $\Phi$ 以标准方式表示为NFA，这种方法先验地会导致双重指数爆炸。然而，近期文献表明，存在某些自动结构类，通过将全称量词视为"一等公民"而非依赖双重补运算，可采用不同方式消去全称量词而避免这种爆炸。虽然现有对某些自动结构类的下界表明，消去一个全称量词时单重指数爆炸不可避免，但尚不清楚是否存在更优方法——即便在受限场景下——避免朴素的双重指数爆炸。本文对此问题给出否定回答：我们构造了一族表示自动关系的NFA，使得在消去单个全称量词后识别该语言的最小NFA具有双重指数规模，且判定该语言是否为空的复杂度为ExpSpace-完全。