AI 中文总结
该研究证明三变量逻辑到关系演算的翻译必然产生指数规模膨胀，通过构造单量词正公式并利用有限结构上的保持论证，解决了长期开放问题，并推广至MATLANG等场景。
AI 中文摘要
三变量一阶逻辑（FO3）与关系演算（CoR）定义相同的二元查询，这一等价性可追溯至20世纪40年代塔斯基的研究。虽然经典的从FO3到CoR的翻译是指数规模的，但我们证明这种规模膨胀是不可避免的，从而解决了一个长期悬而未决的问题。我们构造了带单个量词的正公式φ，其等价项即使在有限结构及具有子项共享的电路表示下，也需要规模2^{Ω(|φ|)}。我们的证明使用了对单个有限结构的保持论证。该方法不仅适用于我们的首要问题，还建立了针对特定规模电路和有界误差随机化电路的下界，并为矩阵查询语言MATLANG产生了类似的指数差距。
英文摘要
Three-variable first-order logic (FO3) and the calculus of relations (CoR) define the same binary queries, an equivalence going back to Tarski in the 1940s. While the classical translation $\text{FO3} \Rightarrow \text{CoR}$ is exponential, we prove that this blow-up is unavoidable, resolving a long-standing open question. We construct positive formulas $φ$ with a single quantifier whose equivalent terms require size $2^{Ω(|φ|)}$, even over finite structures and circuit representations with subterm sharing. Our proof uses a preservation argument over a single finite structure. This approach applies beyond our primary question, establishing the lower bound even for size-specific circuits and bounded-error randomized circuits, and yielding an analogous exponential gap for the matrix query language MATLANG.
