Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Collapsing Constructive and Intuitionistic Modal Logics

Leonardo Pacheco

Abstract

We prove that the constructive and intuitionistic variants of the modal logic $\mathsf{KB}$ coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of $\mathsf{K}$ do not prove the same diamond-free formulas.

Collapsing Constructive and Intuitionistic Modal Logics

Abstract

We prove that the constructive and intuitionistic variants of the modal logic coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of do not prove the same diamond-free formulas.
Paper Structure (10 sections, 15 theorems, 8 equations, 3 figures)

This paper contains 10 sections, 15 theorems, 8 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Outline
  3. Acknowledgements
  4. Preliminaries
  5. Syntax
  6. Semantics
  7. Completeness for CKB and IKB
  8. Soundness
  9. Canonical model for CKB
  10. Conclusion

Key Result

Theorem 3

$\mathsf{CKB}\vdash DP$ and $\mathsf{CKB}\vdash N$.

Figures (3)

  • Figure 1: Schematics for forward and backward confluence, respectively. Solid arrows correspond to the universal quantifiers and dashed arrows correspond to the existential quantifiers.
  • Figure 2: The $\mathsf{CK}$-model $M$ from Proposition \ref{['prop::confluence-is-necessary-kb']}, whose modal relation is symmetric but not forward confluent. $B_\Box$ fails at $w$.
  • Figure 3: The outline of the proof of Theorem \ref{['thm::completeness-CKB-IKB']}.

Theorems & Definitions (34)

  • Definition 1
  • Definition 2
  • Theorem 3: Arisaka, Das, Straß burger arisaka2015nested
  • proof
  • Definition 4
  • Definition 5
  • Proposition 6
  • proof
  • Definition 7
  • Theorem 8
  • ...and 24 more