Variable-ordering fragments of first-order logic
Ian Pratt-Hartmann, University of Manchester and Uniwersytet Opolski
In the context of first-order logic, a ‘variable-ordering fragment’ is a subset of formulas identified by restricting the permitted sequences of variables appearing as arguments of atomic subformulas. Examples include W.V.O. Quine’s ‘fluted fragment’, A. Herzig’s ‘forward fragment’ and the recently identified ‘adjacent fragment’. All three of these fragments possess the finite model property and hence are decidable for satisfiability. The largest of these, the adjacent fragment, extends a wide range of propositional modal logics (under the standard translation into first-order logic) as well as the two-variable fragment.
In this talk, I shall give an overview of the possible variable-ordering fragments, and explain how bounds on complexity of satisfiability can be derived. I shall also survey various extensions of these logics, in particular with counting quantification.