Binding forms in first-order logic

Conference item

Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order restrictions proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and ΣP3, respectively.

Authors: Mogavero, F; Perelli, G

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl
• Host title: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
• Journal: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
• Publication date: 2015-09-04
• DOI: 10.4230/LIPIcs.CSL.2015.648
• ISSN: 1868-8969
• ISBN: 9783939897903
• Keywords: SBTMR