日々の流転

λ. 様相論理のシーケント計算

First Steps in Modal Logic はずっとヒルベルト流の演繹体系で通してたので知らなかったが、論理と計算のしくみ(萩谷 昌己/西崎 真也) で様相論理にもシーケント計算での証明系があることを知る。やっぱりあるのね。これは通常の命題論理のシーケント計算に、以下の必然化の推論規則を追加したもの。

A1, …, An ├ B
─────────────── (必然化)
□A1, …, □An, Γ ├ Δ, □B

ちなみに、First Steps in Modal Logic でのヒルベルト流の必然化の推論規則は以下のようなものだったので、少し趣が異なっている*1。

φ
─── (Ni)
□φ

さらに、ワンのアルゴリズムを拡張した決定手続きも載っていた。いいね。

ただ、ここでは素の様相論理のシーケント計算だけしか載っていなくて、様々な公理を追加したときにどうするかというのが分からなかった。 T(φ) := □φ→φ の形の論理式を公理として追加した場合には簡単で、以下のような推論規則を追加すればよいのだと思う。

Γ, □φ, φ ├ Δ
──────────
Γ, □φ ├ Δ

しかし、4(φ) := □φ→□□φ のような形の論理式や、より一般的な (i,j,k,l)-confluence <i>[j]φ→[k]<l>φ の場合には、どのように追加すれば良いかは良くわからなかった。例えば、4に対応する推論規則として以下を追加すると、前述の決定手続きがうまく働かなくなりそう……*2

Γ ├ Δ, □□φ, □φ
────────────
Γ ├ Δ, □□φ

私はシーケント計算とか良く知らないのだけど、シーケント計算に詳しい人にはこういうのもすぐわかったりするのだろうか。あと、様相論理の証明系の話とかは頭腐の宮本賢治さんが詳しそうだなぁ……

8/7 追記

線形論理の ! がS4様相だという話を思い出した。 4に関しては ! の規則と同様に以下のような推論規則にすれば良いはず。

□Γ ├ φ
──────
□Γ ├ □φ

ただ、5(φ) := ◇φ → □◇φ に関してはこんな風にはいかなそう。 Deep Inference and the Calculus of Structures - Modal Logic にある“The Design of Modal Proof Theories: The Case of S5”を見ると、カット除去が成り立つような S5 の推論規則にはやはり deep inference が必要なようだ。