Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fusions of One-Variable First-Order Modal Logics

Roman Kontchakov, Dmitry Shkatov, Frank Wolter

TL;DR

Fusions of one-variable modal logics are viewed as fusions of propositional modal logics sharing an S5 modality and provide a general sufficient condition for transfer of Kripke completeness and decidability (but not of finite model property).

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 (but not of finite model property).

Fusions of One-Variable First-Order Modal Logics

TL;DR

Fusions of one-variable modal logics are viewed as fusions of propositional modal logics sharing an S5 modality and provide a general sufficient condition for transfer of Kripke completeness and decidability (but not of finite model property).

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 (but not of finite model property).
Paper Structure (9 sections, 20 theorems, 48 equations, 1 figure)

This paper contains 9 sections, 20 theorems, 48 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Fusions of Equality-Free One-Variable Logics
  4. Global Consequence
  5. Local Consequence
  6. Fusions of One-Variable Logics with Equality
  7. Fusions of Propositional Modal Logics Sharing an S5 Modality
  8. Discussion
  9. Proof of Lemma \ref{['lem:one-var-vs-prop']}

Key Result

Theorem 1

Kripke completeness and decidability are preserved under fusions of Kripke complete one-variable first-order modal logics, for both the local and global consequence and expanding and constant domain semantics. The finite model property is preserved for the local consequence but not for global conseq

Figures (1)

  • Figure 1: Proof of Theorem \ref{['thm:nontransfer1']}. a) Formula $\textsf{card}(I,P)$. b) Equation $e$ of the form $y = z_1 \times z_2$ with $z_1 = 3$ and $z_2 = 2$ (only worlds in $W$ and their domains are shown).

Theorems & Definitions (36)

  • Theorem 1: Equality-Free Fusion
  • Theorem 2: Fusion with Equality
  • Theorem 3: Propositional Fusion with Shared S5
  • Lemma 2.1
  • Theorem 3.1
  • Lemma 3.2
  • proof
  • Definition 3.3
  • Definition 3.4
  • Theorem 3.5
  • ...and 26 more