非正規様相論理

非正規様相論理は、正規様相論理の基本原理から逸脱した様相論理の変種です。

通常の様相論理は、分配公理 ( ) と「トートロジーは必然的に真でなければならない」 ( を伴意する) とを述べる必然性原理に従います。^[1]一方、非正規様相論理は、常にそのような要件を持つわけではありません。 非正規様相論理の最小の変種は論理Eであり、これは、古典的な命題論理の対応する証明システムに対するヒルベルト計算に合同規則、またはそのシーケント計算にE規則を含みます。 追加の公理、つまり公理M、C 、およびNを追加して、より強力な論理システムを形成できます。 3 つの公理すべてを論理Eに追加すると、通常の様相論理Kと同等の論理システムが得られます。^[2]${\displaystyle \Box (p\to q)\to (\Box p\to \Box q)}$${\displaystyle \vdash A}$${\displaystyle \vdash \Box A}$

クリプキ意味論は正規様相論理（例えば、論理K ）の最も一般的な形式意味論ですが、非正規様相論理は近傍意味論で解釈されることが多いです。

非正規様相論理システムの構文は、命題論理に基づく正規様相論理の構文に似ています。原子ステートメントは命題変数 (例) で表され、論理接続子には否定 ( )、連言 ( )、選言 ( )、含意 ( ) が含まれます。様相は、ボックス ( ) とダイヤモンド ( )で最も一般的に表されます。 ${\displaystyle p,q,r}$${\displaystyle \neg}$${\displaystyle \land}$${\displaystyle \lor}$${\displaystyle \to }$${\displaystyle \Box }$${\displaystyle \Diamond }$

この構文の形式文法は、否定、選言、ボックス記号のみを使用して最小限定義できます。このような言語では、 は任意の命題名です。^[3]結合はと同等として定義できます。任意の様相論理式 に対して、式はによって定義されます。あるいは、言語が最初にダイヤモンドで定義されている場合、ボックスは によって同様に定義できます。^[4]${\displaystyle \varphi ,\psi :=p\ |\ \neg \varphi \ |\ \Box \varphi \ |\ \varphi \lor \psi }$${\displaystyle p}$${\displaystyle \varphi \land \psi }$${\displaystyle \neg (\neg \varphi \lor \neg \psi )}$${\displaystyle \varphi }$${\displaystyle \Diamond \varphi }$${\displaystyle \neg \Box \neg \varphi }$${\displaystyle \Box \varphi \equiv \neg \Diamond \neg \varphi }$

任意の命題名について、式および は命題リテラルとみなされ、およびは様相リテラルとみなされます。 ${\displaystyle p}$${\displaystyle p}$${\displaystyle \neg p}$${\displaystyle \Box p}$${\displaystyle \neg \Box p}$

非正規様相論理の最小変種である論理Eには、ヒルベルト計算にRE合同規則が含まれるか、シーケント計算に E規則が含まれます。

論理Eのヒルベルト計算は、合同規則 ( RE ) を持つ古典的な命題論理のヒルベルト計算に基づいて構築されています。あるいは、規則は によって定義することもできます。この規則を含む論理は合同型と呼ばれます。 ${\displaystyle {\frac {A\leftrightarrow B}{\Box A\leftrightarrow \Box B}}}$${\displaystyle {\frac {A\leftrightarrow B}{\Diamond A\leftrightarrow \Diamond B}}}$

論理Eのシークエント計算は、シークエント上で動作する別の証明システムであり、命題論理の推論規則と 推論のE規則で構成されます。 ${\displaystyle {\frac {A\vdash B\qquad B\vdash A}{\Gamma ,\Box A\vdash \Box B,\Delta }}}$

後続の手段は を伴い、は先行詞（前提としての公式の連言）であり、 は先例（結論としての公式の選言） である。${\displaystyle \Gamma \vdash \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$

非正規様相論理の解決計算では、大域様相と局所様相の概念が導入されている。式は様相式の大域様相を表し、これは近傍モデル内のすべての世界で成り立つことを意味する。論理Eの場合、解決計算はLRES、GRES、G2L、LERES、GERES規則から構成される。^[3]${\displaystyle {\mathsf {G}}(\varphi )}$${\displaystyle \varphi }$${\displaystyle \varphi }$

LRES 規則は、命題リテラルとが削除される古典的な命題論理の解決規則に似ています。 ${\displaystyle p}$${\displaystyle \neg p}$${\displaystyle {\frac {D\lor l\qquad D'\lor \neg l}{D\lor D'}}}$

LERES ルールは、2 つの命題名とが同等である場合、およびは削除できると規定しています。G2L ルールは、グローバルに真である式はローカルにも真であると規定しています。GRES および GERES 推論ルールは、LRES および LERES のバリエーションですが、グローバル モダリティを特徴とする式に適用されます。 ${\displaystyle p}$${\displaystyle p'}$${\displaystyle \Box p}$${\displaystyle \neg \Box p'}$

任意の様相式が与えられた場合、この解決計算による証明プロセスは、複雑な様相式を命題名として再帰的に名前変更し、グローバル様相を使用してそれらの同等性を主張することによって実行されます。

クリプキ意味論は正規様相論理の意味論としてよく適用されるが、非正規様相論理の意味論は一般に近傍モデルで定義される。標準的な近傍モデルは、以下の3つで定義される。^{[5] [6]}${\displaystyle {\mathcal {M}}}$${\displaystyle \langle {\mathcal {W}},{\mathcal {N}},{\mathcal {V}}\rangle }$

• ${\displaystyle {\mathcal {W}}}$は空でない世界の集合です。
• ${\displaystyle {\mathcal {N}}:{\mathcal {W}}\to {\mathcal {PP}}({\mathcal {W}})}$は、任意の世界を世界の集合にマッピングする近傍関数です。この関数は、べき集合を表します。${\displaystyle {\mathcal {P}}}$
• ${\displaystyle {\mathcal {V}}:Atm\to {\mathcal {P}}({\mathcal {W}})}$は、任意の命題名が与えられたときに、が真となる世界の集合を出力する評価関数です。${\displaystyle p}$${\displaystyle p}$

この意味論は、さらに二近傍意味論として一般化することができる。^[7]

非正規様相論理の古典的立方体は、次のように定義される論理Eに追加できる公理M、C、Nを考慮します。^[6]

公理M を含む論理システムは単調です。公理 M と C を使用すると、論理システムは正則になります。3 つの公理すべてを含めると、論理システムは正規になります。

これらの公理に応じて、追加のルールが証明システムに組み込まれます。