Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics

Yuki Nishimura

TL;DR

This work develops sound and complete internalized tableau calculi for two-dimensional hybrid product logic ($HPL$) and hybrid dependent product logic ($HdPL$), built on product and dependent Kripke frames. It proves soundness and completeness for both logics on their respective frame classes, and introduces a decreasing-frame refinement for HdPL via a special [Dec] rule. Despite these strong results, the calculi lack termination in general, leaving decidability of $HPL$ open and posing challenges for larger dimensions or richer operators. The paper also extends the framework to HdPL, shows how frame dependence affects semantics and tableaux, and discusses future directions like termination strategies, higher dimensions, additional operators, and axioms. Overall, it advances a robust tableau-based approach for multi-dimensional hybrid logics, with concrete guidance for extending to more complex modalities and frame conditions.

Abstract

Hybrid logic is one of the extensions of modal logic. The many-dimensional product of hybrid logic is called hybrid product logic (HPL). We construct a sound and complete tableau calculus for two-dimensional HPL. Also, we made a tableau calculus for hybrid dependent product logic (HdPL), where one dimension depends on the other. In addition, we add a special rule to the tableau calculus for HdPL and show that it is still sound and complete. All of them lack termination, however.

Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics

TL;DR

This work develops sound and complete internalized tableau calculi for two-dimensional hybrid product logic () and hybrid dependent product logic (), built on product and dependent Kripke frames. It proves soundness and completeness for both logics on their respective frame classes, and introduces a decreasing-frame refinement for HdPL via a special [Dec] rule. Despite these strong results, the calculi lack termination in general, leaving decidability of open and posing challenges for larger dimensions or richer operators. The paper also extends the framework to HdPL, shows how frame dependence affects semantics and tableaux, and discusses future directions like termination strategies, higher dimensions, additional operators, and axioms. Overall, it advances a robust tableau-based approach for multi-dimensional hybrid logics, with concrete guidance for extending to more complex modalities and frame conditions.

Abstract

Hybrid logic is one of the extensions of modal logic. The many-dimensional product of hybrid logic is called hybrid product logic (HPL). We construct a sound and complete tableau calculus for two-dimensional HPL. Also, we made a tableau calculus for hybrid dependent product logic (HdPL), where one dimension depends on the other. In addition, we add a special rule to the tableau calculus for HdPL and show that it is still sound and complete. All of them lack termination, however.
Paper Structure (15 sections, 24 theorems, 28 equations, 5 figures)

This paper contains 15 sections, 24 theorems, 28 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Kripke Semantics of Hybrid Product Logic
  3. Internalized Tableau
  4. Soundness
  5. Completeness
  6. Hybrid Dependent Product Logic (HdPL)
  7. Frames and Models
  8. Tableau Calculus for HdPL
  9. Soundness and Completeness
  10. Restrictions on Frames
  11. Conclusions and Future Work
  12. Termination and Decidability
  13. What if We Have More Dimensions?
  14. Adding More Operators
  15. Adding More Rules

Key Result

Lemma 4.2

Let $\Theta = \Theta^m$ be a fragment of a branch and $\mathfrak{M} = (\mathfrak{F}, V)$ a model that is faithful to $\Theta^m$. Let $\Theta^{m+1}$ be a new branch (possibly not the only one) that we acquire by applying one of the rules to $\Theta^m$. Then, there exists a model $\mathfrak{M}'=(\math

Figures (5)

  • Figure 1: A product Kripke model.
  • Figure 2: The rules of the tableau calculus for HPL.
  • Figure 3: An example of a d-product frame in the proof of Lemma \ref{['propswap']}.
  • Figure 4: A tableau for HdPL that proves (\ref{['axdec']}).
  • Figure 5: An example of a tableau for HPL that has an infinite branch.

Theorems & Definitions (73)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Remark 3.4
  • Definition 3.5: provability
  • ...and 63 more