The Complexity of Decomposing Modal and First-Order Theories

We show that the satisfiability problem for the two-dimensional extension KxK of unimodal K is nonelementary, hereby confirming a conjecture of Marx and Mikulas from 2001. Our lower bound technique allows us to derive further lower bounds for many-dimensional modal logics for which only elementary lower bounds were previously known. We also derive nonelementary lower bounds on the sizes of Feferman-Vaught decompositions w.r.t. product for any decomposable logic that is at least as expressive as unimodal K. Finally, we study the sizes of Feferman-Vaught decompositions and formulas in Gaifman normal form for fixed-variable fragments of first-order logic.