Marie Fortin (IRIF, CNRS), FO = FO^3 for Linear Orders with Monotone Binary Relations



It is well-known that linear orders have the 3-variable property, meaning that over linear orders, every monadic first-order formula with up to 3 free variables is equivalent to one that uses at most 3 variables in total. This is usually shown through Ehrenfeucht–Fraïssé games, or as a corollary of the expressive completeness of linear temporal logic (with Stavi connectives). Over the years, this has been extended to richer classes of structures, such as the real line with the +1 relation, Mazurkiewicz traces, or message sequence charts. In this talk, I will present a unifying proof that generalizes those facts. It is based on star-free PDL, a variant of propositional dynamic logic that is closely related to Tarski’s calculus of relations and captures precisely the 3-variable fragment of first-order logic. More precisely, I will show that over structures consisting of one linear order and arbitrarily many binary relations satisfying some monotonicity conditions, star-free PDL has the same expressive power as full first-order logic. This implies that any class of such structures has the 3-variable property.