2025-11-21T13:49:15.584467

Twist Sequent Calculi for S4 and its Neighbors

Kamide

Two Gentzen-style twist sequent calculi for the normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ the standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Using these calculi, short proofs can be generated for provable negated modal formulas that contain numerous negation connectives. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained. Additionally, Gentzen-style twist (hyper)sequent calculi for other normal modal logics including S5 are considered.

academic

S4とその周辺に対するツイスト列計算

基本情報

論文ID: 2501.00483
タイトル: Twist Sequent Calculi for S4 and its Neighbors
著者: 神出伸宏（名古屋市立大学データ科学部、愛知県、日本）
分類: cs.LO（コンピュータ科学における論理）
発表会議: Non-Classical Logics: Theory and Applications (NCL'24), EPTCS 415, 2024
論文リンク: https://arxiv.org/abs/2501.00483

要旨

本論文は、正規様相論理S4に対するGentzen様式のツイスト列計算(twist sequent calculi)の2つの変種を提案し研究する。提案された演算体系は、否定結合子に対する標準的な論理推論規則を使用せず、代わりに否定論理結合子に対するツイスト論理推論規則を採用している。これらの演算体系を用いることで、多くの否定結合子を含む証明可能な否定様相公式に対して簡潔な証明を生成することができる。本論文は、これらの演算の切除定理を証明し、部分公式性質を得た。さらに、他の正規様相論理（S5を含む）に対するGentzen様式のツイスト（超）列計算も検討している。

研究背景と動機

問題定義

本研究が解決しようとする中核的な問題は、多くの否定結合子を含む様相公式に対して、効果的かつ簡潔な証明体系をいかに提供するかである。従来のGentzen様式列計算は、複数の否定を含む様相公式を処理する際に冗長な証明を生成する。

研究の重要性

哲学論理的意義：否定情報または知識の推論、特に否定と様相を含む推論は、Fitch逆説の分析など、哲学論理の分野で重要な意義を持つ。
コンピュータ科学への応用：論理プログラミングと知識表現において、様相と否定を含む推論は極めて重要である。
証明効率：現実世界では、真の否定情報は通常、様相演算子と複数の否定結合子を含む証明可能な否定様相公式によって表現され、証拠としての簡潔な証明が必要とされる。

既存手法の限界

大西-松本体系：切除自由かつ分析的であるが、多くの否定結合子を含む否定様相公式の証明において効率が低い。
Kripkeの GS4 体系：同様に証明が冗長になる問題がある。
その他の拡張体系（NS4、DS4、SS4、GS41-GS43）：特定の推論タイプに適用可能であるが、分析性を欠くか、否定様相公式の処理において効率が低い。

核心的貢献

2つのツイスト列計算の提案：lTS4（局所ツイスト）と gTS4（大域ツイスト）を提案し、両者とも切除自由かつ分析的である。
証明論的結果：切除定理と部分公式性質を確立した。
効率の向上：多くの否定結合子を含む様相公式に対して著しく短い証明を提供する。
他の様相論理への拡張：K、KT、S5などの他の正規様相論理に対応するツイスト演算を構築した。
理論的等価性：lTS4、gTS4と標準的なGS4体系の定理等価性を証明した。

方法の詳細

タスク定義

Gentzen様式の列計算体系を構築し、正規様相論理S4における多くの否定結合子を含む公式に対して簡潔な証明を提供できるようにする。入力は様相公式であり、出力はその公式の証明（証明可能な場合）である。

モデルアーキテクチャ

lTS4（局所ツイスト列計算）

初期列：

標準的：p ⇒ p（任意の命題変数pに対して）
否定：¬p ⇒ ¬p、¬p, p ⇒、⇒ ¬p, p

構造推論規則：

切除規則：(Γ ⇒ α)(α, Γ ⇒ Δ) / (Γ ⇒ Δ)
弱化規則：左弱化および右弱化

非ツイスト論理推論規則：

標準的な∧、∨、→規則
様相規則：(□left)、(□right)、(◊left)、(◊right)

ツイスト論理推論規則：重要な革新はツイスト規則にあり、例えば：

(¬□leftₜ): (Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂, α) / (¬□α, Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂)

gTS4（大域ツイスト列計算）

gTS4は lTS4 の特定の規則を大域ツイスト規則で置き換えることで得られる：

(¬□leftₜ): (Γ₁, Δ₂ ⇒ ◊Δ₁, ◊Γ₂, α) / (¬□α, Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂)

技術的革新点

ツイスト規則の設計：標準的な否定規則を他の論理結合子の規則と統合し、「ショートカット」規則を形成する。
局所対大域処理：lTS4は否定を局所的に処理し（主要でない文脈の否定を保持）、gTS4は大域的に処理する（すべての文脈の否定を削除）。
標準否定規則の排除：Gentzen LK体系の標準的な否定規則(¬left)と(¬right)の使用を完全に回避する。

実験設定

理論検証方法

本論文は数学的証明方法を用いて理論的結果を検証し、主に以下を含む：

帰納的証明：基本的性質と等価性の証明に用いられる
構成的証明：具体的な証明変換を示す
ケース分析：具体例を通じて異なる体系の証明長を比較

評価指標

証明長：異なる体系で生成された証明ステップ数の比較
部分公式性質：証明に現れるすべての公式が結論公式の部分公式であること
切除可能性：体系の切除自由性

実験結果

主要な結果

定理等価性（定理3.3）

lTS4、gTS4と標準的なGS4体系の定理等価性を証明した： {S | lTS4 ⊢ S} = {S | gTS4 ⊢ S} = {S | GS4 ⊢ S}

切除定理（定理4.4）

lTS4とgTS4に対して、切除規則は切除自由体系において許容可能である。

部分公式性質（定理4.5）

lTS4とgTS4は両者とも部分公式性質を有し、体系の分析性を保証する。

ケース分析

例3.5：証明可能な列¬¬¬◊¬p ⇒ ¬◊¬¬□¬¬¬pを考える

lTS4による証明（7ステップ）：

¬p ⇒ ¬p
¬p, ¬◊¬p ⇒ (¬◊leftₜ)
¬¬¬p, ¬◊¬p ⇒ (¬¬leftₜ)
◊¬¬¬p, ¬◊¬p ⇒ (◊left)
¬¬□¬¬¬p, ¬◊¬p ⇒ (¬¬leftₜ)
¬◊¬p ⇒ ¬◊¬¬□¬¬¬p (¬◊rightₜ)
¬¬¬◊¬p ⇒ ¬◊¬¬□¬¬¬p (¬¬leftₜ)

gTS4による証明（7ステップ）：同様に簡潔な証明

GS4による証明（14ステップ）：標準的な否定規則を用いた冗長な証明