Three-variable first-order logic ($\mathrm{FO}^3$) and the calculus of relations (CoR) define the same binary queries, an equivalence that goes back to Tarski's work in the 1940s. The classical translation from $\mathrm{FO}^3$ to CoR is single-exponential, but it has remained open whether this blowup is necessary. We prove that it is, even over finite structures and even for circuits that share subterms. Our proof introduces a new technique: we modify a single finite structure in exponentially many local ways, each changing the answer of a short $\mathrm{FO}^3$ formula $\varphi$. In any CoR circuit $C$ equivalent to $\varphi$, only compositions of binary relations can notice these modifications, and each composition can notice at most two; thus, $C$ requires exponentially many compositions. The same technique gives an exponential succinctness gap between $\mathrm{FO}^3$ and $\mathrm{FO}^2$, and exponential lower bounds for matrix query languages over the Boolean and tropical semirings, where the analogous question was also open.

翻译：暂无翻译