An Exponential Succinctness Gap between Three-Variable Logic and the Calculus of Relations
En palabras de los autores
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 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 , 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.
Apareció: miércoles, 23 de septiembre. arXiv. Preprint, todavía sin revisión por pares.