Automatic structures are first-order 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}. Φ\equiv \neg (\exists{x}. \neg Φ)$. If $Φ$ 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ïve 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. The techniques underlying our EXPSPACE lower bound further enable us to establish new lower bounds for some fragments of Büchi arithmetic with a fixed number of quantifier alternations.

翻译：自动结构是那些论域和关系可表示为正则语言的一阶结构。根据正则语言的标准闭包性质，自动结构的一阶理论是可判定的。虽然存在量词可通过同态应用在线性时间内消去，但全称量词通常通过恒等式 $\forall{x}. Φ\equiv \neg (\exists{x}. \neg Φ)$ 消去。若 $Φ$ 以标准方式表示为 NFA，则该方法先验地会导致双重指数膨胀。然而，近期文献表明，存在一些自动结构类，其全称量词可通过不同方法作为"一等公民"处理而避免这种膨胀，无需依赖双重补运算。虽然现有针对某些自动结构类的下界表明，消去全称量词时单指数膨胀不可避免，但尚不清楚是否存在更好的方法能避免朴素的双重指数膨胀，至少在受限场景下可能实现。本文对此问题给出否定答案，证明存在一族表示自动关系的 NFA，消去单个全称量词后识别该语言的最小 NFA 具有双重指数规模，且判定该语言是否为空是 EXPSPACE 完全的。我们建立 EXPSPACE 下界的技术进一步使我们能为具有固定量词交替次数的布赫算术片段确立新的下界。