Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Intrinsic and relative characterization results for logics with negative modalities

Jim de Groot, João Marcos, Rodrigo Stefanes

TL;DR

The paper investigates expressive power in modal languages that include subclassical negations and restoration operators. It develops a parametric notion of simulations (Λ-simulations) and proves Hennessy-Milner-type intrinsic and Van Benthem-type relative characterizations for modally saturated models. Key contributions include precise invariance results, undefinability phenomena for classical negation in minimal restorative logics, and groundwork for symmetrical and combined modalities. The work clarifies how restoration connectives recover classical reasoning within a broadly expressive modal framework and connects these findings to potential coalgebraic and combined-modal extensions.

Abstract

We introduce simulations for modal logics with subclassical negations and restoration modalities, establish an adequacy theorem, and prove intrinsic (Hennessy-Milner-type) and relative (Van Benthem-type) characterization results. These results identify each restorative language with the fragment of first-order logic invariant under its simulations and delineate the expressive profile of modal logics with non-classical negations.

Intrinsic and relative characterization results for logics with negative modalities

TL;DR

The paper investigates expressive power in modal languages that include subclassical negations and restoration operators. It develops a parametric notion of simulations (Λ-simulations) and proves Hennessy-Milner-type intrinsic and Van Benthem-type relative characterizations for modally saturated models. Key contributions include precise invariance results, undefinability phenomena for classical negation in minimal restorative logics, and groundwork for symmetrical and combined modalities. The work clarifies how restoration connectives recover classical reasoning within a broadly expressive modal framework and connects these findings to potential coalgebraic and combined-modal extensions.

Abstract

We introduce simulations for modal logics with subclassical negations and restoration modalities, establish an adequacy theorem, and prove intrinsic (Hennessy-Milner-type) and relative (Van Benthem-type) characterization results. These results identify each restorative language with the fragment of first-order logic invariant under its simulations and delineate the expressive profile of modal logics with non-classical negations.

Paper Structure

This paper contains 26 sections, 19 theorems, 19 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Negative modalities over a positive basis.
  3. Restorative modal logics.
  4. Bisimulations.
  5. Simulations.
  6. Contributions.
  7. Structure of the paper.
  8. Negative modalities and their restoration companions
  9. Negations of all flavors.
  10. Classical and normal modal logics.
  11. Standard connectives, positive and negative modalities.
  12. Restoration connectives.
  13. Kripke semantics for modal logics
  14. Modal logic as you know it
  15. Interpreting negative modalities and their restoration companions
  16. ...and 11 more sections

Key Result

Proposition 3.6

Let $\mathfrak{M}_1 = \langle W_1, R_1,\{P_{k,1}\}_{k\in K}\rangle$ and $\mathfrak{M}_2 = \langle W_2, R_2,\{P_{k,2}\}_{k\in K}\rangle$ be two Kripke models, and for each $\ell \in \{ 1, 2 \}$ let $\mathop{\mathrm{in}}\nolimits_\ell : \mathfrak{M}_\ell \to \mathfrak{M}_1 \uplus \mathfrak{M}_2$ be th

Figures (7)

  • Figure 1: Square of Oppositions involving positive and negative modalities.
  • Figure 2: Squares of Oppositions containing the restoration companions of the subclassical negations. The top squares represent the legitimacy conditions; at the bottom, the left square contains the basic restorative conditions and the right square supplements them with the standard restorative conditions.
  • Figure 3: The simulation conditions can be depicted in diagrammatic form. The modal accessibility relation is depicted with an arrow, while the simulation relation is drawn as a bullet-headed arrow. Solid arrows indicate universal quantification, and the dashed and dotted arrows existential ones. The dashed and dotted lines should be read as a disjunction: either the connections indicated by the dotted lines hold, or the connection indicated by the dashed line holds.
  • Figure 4: Depictions of the models and simulations from Examples \ref{['exm:smile-vsmile']} and \ref{['exm:neg']}. Here, the bullet-headed arrows indicate a connection in the relation $\text{S}$. The highlighted area gives information on the truth sets of the propositional letters: in the left picture these truth sets are all empty; in the right picture we hightlight the truth set of the propositional letter $p_\star$, all other truth sets being empty again.
  • Figure 5: Depiction of the model from Example \ref{['exm:dashed']}. The highlighted area shows the truth sets of all propositional letters. The bullet-headed arrow indicates our desired simulation connection, and the dotted arrows indicate the required connections (that we do not have).
  • ...and 2 more figures

Theorems & Definitions (50)

  • Definition 3.1
  • Definition 3.2
  • Remark 3.3
  • Remark 3.4
  • Definition 3.5
  • Proposition 3.6
  • Definition 3.7
  • Definition 3.8
  • Proposition 3.9
  • Remark 3.10
  • ...and 40 more