2025/04/29 by Louwe B. Kuijer, Tony Tan, Kuijer, Louwe +5 · 4 citations
Computer Science · #03B45 (Primary) 03C40 (Secondary) #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2504.20491
openalex publication_date 2025/04/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
For fragments L of first-order logic (FO) with counting quantifiers, we consider the definability problem, which asks whether a given L-formula can be equivalently expressed by a formula in some fragment of L without counting, and the more general separation problem asking whether two mutually exclusive L-formulas can be separated in some counting-free fragment of L. We show that separation is undecidable for the two-variable fragment of FO extended with counting quantifiers and for the graded modal logic with inverse, nominals and universal modality. On the other hand, if inverse or nominals are dropped, separation becomes coNExpTime- or 2ExpTime-complete, depending on whether the universal modality is present. In contrast, definability can often be reduced in polynomial time to validity in L. We also consider uniform separation and show that it often behaves similarly to definability.