Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nested-sequent Calculus for Modal Logic MB

Tomoaki Kawano

TL;DR

This paper develops a nested-sequent calculus framework $\mathbf{NSMB}$ for the modal quantum-logic MB, addressing gaps in previous Hilbert-style analyses by establishing cut-elimination, completeness, and decidability. It defines MB with $\square^{c}_{\alpha}$ and $\square^{o}_{\alpha}$ over finite index sets $J\subseteq [0,1]$, and bases semantics on $I$-valued relations $R$ within MB-realizations, ensuring symmetry and probabilistic interpretation. The main contribution is a rigorously proven calculus that yields a finite-model property and decidability for MB, with an extension $\mathbf{NSMB^+}$ handling MB+ (MB with new modal symbols) and preserving soundness and completeness. Together, these results provide a solid proof-theoretic foundation for MB and MB+, enabling reliable analysis of quantum-logical modalities and their computational properties.

Abstract

Quantum logic (QL) is a non-classical logic for analyzing the propositions of quantum physics. Modal logic MB, which is a logic that handles the value of the inner product that appears in quantum mechanics, was constructed with the development of QL. Although the basic properties of this logic have already been analyzed in a previous study, some essential parts still need to be completed. They are concerned with the completeness theorem and the decidability of the validity problem of this logic. This study solves those problems by constructing a nested-sequent calculus for MB. In addition, new logic MB+ with the addition of new modal symbols is discussed.

Nested-sequent Calculus for Modal Logic MB

TL;DR

This paper develops a nested-sequent calculus framework for the modal quantum-logic MB, addressing gaps in previous Hilbert-style analyses by establishing cut-elimination, completeness, and decidability. It defines MB with and over finite index sets , and bases semantics on -valued relations within MB-realizations, ensuring symmetry and probabilistic interpretation. The main contribution is a rigorously proven calculus that yields a finite-model property and decidability for MB, with an extension handling MB+ (MB with new modal symbols) and preserving soundness and completeness. Together, these results provide a solid proof-theoretic foundation for MB and MB+, enabling reliable analysis of quantum-logical modalities and their computational properties.

Abstract

Quantum logic (QL) is a non-classical logic for analyzing the propositions of quantum physics. Modal logic MB, which is a logic that handles the value of the inner product that appears in quantum mechanics, was constructed with the development of QL. Although the basic properties of this logic have already been analyzed in a previous study, some essential parts still need to be completed. They are concerned with the completeness theorem and the decidability of the validity problem of this logic. This study solves those problems by constructing a nested-sequent calculus for MB. In addition, new logic MB+ with the addition of new modal symbols is discussed.
Paper Structure (4 sections, 1 theorem, 7 equations, 1 figure)

This paper contains 4 sections, 1 theorem, 7 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Modal logic MB
  3. Nested-sequent
  4. Nested-sequent calculus NSMB

Key Result

Theorem 3.1

$\hbox{$\mit \Gamma$} \Rightarrow \hbox{$\mit \Delta$}, \mathcal{T}$ is valid iff $\tau(\hbox{$\mit \Gamma$} \Rightarrow \hbox{$\mit \Delta$}, \mathcal{T})$ is valid.

Figures (1)

  • Figure :

Theorems & Definitions (2)

  • Theorem 3.1
  • proof