Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LEGO-like Small-Model Constructions for Åqvist's Logics

Dmitry Rozplokhas

TL;DR

Alternative small model constructions assembled from elementary building blocks are introduced, applicable uniformly to all four {\AA}qvist's logics, which propose alternative semantical characterizations and imply co-NP-completeness of theoremhood.

Abstract

Åqvist's logics (E, F, F+(CM), and G) are among the best-known systems in the long tradition of preference-based approaches for modeling conditional obligation. While the general semantics of preference models align well with philosophical intuitions, more constructive characterizations are needed to assess computational complexity and facilitate automated deduction. Existing small model constructions from conditional logics (due to Friedman and Halpern) are applicable only to F+(CM) and G, while recently developed proof-theoretic characterizations leave unresolved the exact complexity of theoremhood in logic F. In this paper, we introduce alternative small model constructions assembled from elementary building blocks, applicable uniformly to all four Åqvist's logics. Our constructions propose alternative semantical characterizations and imply co-NP-completeness of theoremhood. Furthermore, they can be naturally encoded in classical propositional logic for automated deduction.

LEGO-like Small-Model Constructions for Åqvist's Logics

TL;DR

Alternative small model constructions assembled from elementary building blocks are introduced, applicable uniformly to all four {\AA}qvist's logics, which propose alternative semantical characterizations and imply co-NP-completeness of theoremhood.

Abstract

Åqvist's logics (E, F, F+(CM), and G) are among the best-known systems in the long tradition of preference-based approaches for modeling conditional obligation. While the general semantics of preference models align well with philosophical intuitions, more constructive characterizations are needed to assess computational complexity and facilitate automated deduction. Existing small model constructions from conditional logics (due to Friedman and Halpern) are applicable only to F+(CM) and G, while recently developed proof-theoretic characterizations leave unresolved the exact complexity of theoremhood in logic F. In this paper, we introduce alternative small model constructions assembled from elementary building blocks, applicable uniformly to all four Åqvist's logics. Our constructions propose alternative semantical characterizations and imply co-NP-completeness of theoremhood. Furthermore, they can be naturally encoded in classical propositional logic for automated deduction.
Paper Structure (13 sections, 18 theorems, 7 equations, 3 figures)

This paper contains 13 sections, 18 theorems, 7 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Small Model Constructions
  4. Small Model Construction for Logic E
  5. Small Model Construction for Logic F
  6. Small Model Construction for Logic F+(CM)
  7. Small Model Construction for Logic G
  8. Applications
  9. Alternative semantical characterizations
  10. Complexity and automated deduction
  11. Detailed proof of Th. \ref{['lem:rearranged_countermodel_conditions']}
  12. Strong completeness vs finite-modal characterization
  13. Propositional encoding for Å qvist's logics

Key Result

theorem 1

Suppose $M = \langle W, \succeq, \mathbb{V} \rangle$ is a countermodel for $\varphi$ and ${M' = \langle W', \succeq', \mathbb{V}' \rangle}$ rearranges $M$ with the prototype function $prot \colon W' \to W$. Then the following conditions are sufficient for $M' \not\models \varphi$.

Figures (3)

  • Figure 1: Preference-semantical characterizations for Å qvist's logics Xavier_handbook_survey (with maximality as the notion of bestness).
  • Figure 2: Small model constructions for Å qvist's logics. Gray circles represent worlds, dashed rectangles represent blocks. Symbol inside a block indicates an antichain, indicates a chain, and indicates a clique. Solid arrows represent the preference relation $\succeq _L$ between blocks: an arrow from a block $l_1$ to a block $l_2$ means $l_2 \succeq _L l_1$. The arrow between blocks in construction $\textit{SMC}^{\,\textbf{G}\xspace}(\varphi, M)$ means that there is a linear order on blocks. Note that the preference relation in constructions $\textit{SMC}^{\,\textbf{E}\xspace}(\varphi, M)$ and $\textit{SMC}^{\,\textbf{F}\xspace}(\varphi, M)$ is not transitive.
  • Figure 3: Finite-model characterizations of theoremhood in Å qvist's logics (with maximality as the notion of bestness).

Theorems & Definitions (56)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • theorem 1
  • proof
  • definition 7
  • definition 8
  • ...and 46 more