2026-08-21T18:02:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27453 2026-08-21T14:42:40Z ddc:004 open_access

Order-Invariant Cluster First-Order Logic on Graph Classes of Bounded Degree Ghasemi, Fatemeh Grange, Julien Order invariance cluster first-order logic model checking We introduce a new logic, called cluster first-order logic, a restricted fragment of first-order logic specifically designed to study order invariance. An order-invariant formula is one on a vocabulary that contains an order; however, whether a structure satisfies it or not is independent of the interpretation of the order. We show that while order-invariant cluster first-order logic can define properties outside the scope of plain first-order logic in general, its expressive power is included in that of first-order logic when it comes to classes of bounded degree. We establish this result by explicitly constructing linear orders such that similar structures remain similar when they are expanded with these orders. This similarity-preserving, local-to-global approach is technically involved and somewhat counterintuitive, since adding an order usually reveals distinctions that are otherwise hidden due to the locality of first-order logic. We believe that this work can be a stepping stone toward applying such techniques to plain first-order logic and toward settling the question of the expressive power of order-invariant plain first-order logic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fatemeh Ghasemi and Julien Grange 2026 Is Part Of LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2026.71 urn:nbn:de:0030-drops-274533 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.71 eng https://creativecommons.org/licenses/by/4.0/legalcode