Fusions of One-Variable First-Order Modal Logics
Roman Kontchakov, Dmitry Shkatov, Frank Wolter

TL;DR
This paper studies how combining one-variable first-order modal logics affects properties like completeness and decidability, showing that certain features are preserved without equality but not with it, using Diophantine equations for proofs.
Contribution
It provides new preservation results for fusion of one-variable first-order modal logics, especially regarding equality, completeness, and decidability, with a general transfer condition.
Findings
Kripke completeness and decidability are preserved without equality.
Equality and non-rigid constants break preservation of these properties.
Finite model property is only preserved locally even without equality.
Abstract
We investigate preservation results for the independent fusion of one-variable first-order modal logics. We show that, without equality, Kripke completeness and decidability of the global and local consequence relation are preserved, under both expanding and constant domain semantics. By contrast, Kripke completeness and decidability are not preserved for fusions with equality and non-rigid constants (or, equivalently, counting up to one), again for the global and local consequence and under both expanding and constant domain semantics. This result is shown by encoding Diophantine equations. Even without equality, the finite model property is only preserved in the local case. Finally, we view fusions of one-variable modal logics as fusions of propositional modal logics sharing an S5 modality and provide a general sufficient condition for transfer of Kripke completeness and decidability…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Logic, programming, and type systems
