一般フレーム

論理学において、一般フレーム（または単にフレーム）は、追加の構造を持つクリプキフレームであり、様相論理と中間論理をモデル化するために使用されます。一般フレーム意味論は、クリプキ意味論と代数的意味論の主な長所を組み合わせたもので、前者の透明な幾何学的洞察と後者の堅牢な完全性を共有しています。

様相一般フレームは、3 つの であり、はクリプキ フレーム (つまり、は集合 上の2 項関係)、 は次について閉じている の サブセットの集合です。${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$${\displaystyle \langle F,R\rangle }$${\displaystyle R}$${\displaystyle F}$${\displaystyle V}$${\displaystyle F}$

• ブール演算（二項）積、和、補数、
• によって定義される操作。${\displaystyle \Box }$${\displaystyle \Box A=\{x\in F\mid \forall y\in F\,(x\,R\,y\to y\in A)\}}$

したがって、これらは追加の構造を持つ集合体の特殊なケースである。 の目的は、フレームで許容される値を制限することである。クリプキフレームに基づくモデルは、一般のフレームで許容される。 ${\displaystyle V}$${\displaystyle \langle F,R,\Vdash \rangle }$${\displaystyle \langle F,R\rangle }$${\displaystyle \mathbf {F} }$

${\displaystyle \{x\in F\mid x\Vdash p\}\in V}$すべての命題変数 に対して。${\displaystyle p}$

の閉包条件は、すべての式(変数だけでなく) がに属することを保証します。${\displaystyle V}$${\displaystyle \{x\in F\mid x\Vdash A\}}$${\displaystyle V}$${\displaystyle A}$

式は、すべての許容される値およびすべての点に対して である場合に、で有効です。のすべての公理 (または同等に、すべての定理)が で有効な場合、通常の様相論理はフレーム で有効です。この場合、-フレームと呼びます。 ${\displaystyle A}$${\displaystyle \mathbf {F} }$${\displaystyle x\Vdash A}$${\displaystyle \Vdash }$${\displaystyle x\in F}$ ${\displaystyle L}$${\displaystyle \mathbf {F} }$${\displaystyle L}$${\displaystyle \mathbf {F} }$${\displaystyle \mathbf {F} }$${\displaystyle L}$

クリプキフレームは、すべての評価が許容される一般的なフレーム、つまり と同一視できます。ここで はのべき集合を表します。 ${\displaystyle \langle F,R\rangle }$${\displaystyle \langle F,R,{\mathcal {P}}(F)\rangle }$${\displaystyle {\mathcal {P}}(F)}$${\displaystyle F}$

一般的に言えば、一般フレームはクリプキモデルの派手な名前に過ぎません。特に、様相公理とアクセス可能性関係の特性との対応は失われます。これは、許容可能な評価のセットに追加の条件を課すことで改善できます。

フレームは ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$

• 差別化されている場合、${\displaystyle \forall A\in V\,(x\in A\Leftrightarrow y\in A)}$${\displaystyle x=y}$
• タイト、意味する場合、${\displaystyle \forall A\in V\,(x\in \Box A\Rightarrow y\in A)}$${\displaystyle x\,R\,y}$
• コンパクト、有限交差特性を持つのすべての部分集合が空でない交差を持つ場合、${\displaystyle V}$
• アトミック、すべてのシングルトンを含む場合、${\displaystyle V}$
• 洗練された、差別化された、緊密な、
• 洗練されていて簡潔であれば、説明的であると言えます。

クリプキ フレームは洗練され、原子的です。ただし、無限クリプキ フレームは決してコンパクトではありません。すべての有限微分フレームまたは原子フレームはクリプキ フレームです。

記述フレームは、双対性理論（下記参照）により、最も重要なフレームのクラスです。洗練されたフレームは、記述フレームとクリプキ フレームの共通の一般化として役立ちます。

あらゆるクリプキモデルは一般フレームを誘導する。ここで は次のように定義される。 ${\displaystyle \langle F,R,{\Vdash }\rangle }$ ${\displaystyle \langle F,R,V\rangle }$${\displaystyle V}$

${\displaystyle V={\big \{}\{x\in F\mid x\Vdash A\}\mid A{\hbox{ is a formula}}{\big \}}.}$

生成サブフレーム、 p-モルフィック画像、およびクリプキフレームの互いに素な和の基本的な真理値保存操作は、一般フレームにも類似点がある。フレーム がフレーム の生成サブフレームであるとは、クリプキフレームがクリプキフレームの生成サブフレームである場合（つまり、 が 、およびの下で上向きに閉じたの部分集合である場合）、および ${\displaystyle \mathbf {G} =\langle G,S,W\rangle }$${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$${\displaystyle \langle G,S\rangle }$${\displaystyle \langle F,R\rangle }$${\displaystyle G}$${\displaystyle F}$${\displaystyle R}$${\displaystyle S=R\cap G\times G}$

${\displaystyle W=\{A\cap G\mid A\in V\}.}$

p-射（または有界射）は、から への関数であり、クリプキフレームとのp-射であり、追加の制約を満たす。 ${\displaystyle f\colon \mathbf {F} \to \mathbf {G} }$${\displaystyle F}$${\displaystyle G}$${\displaystyle \langle F,R\rangle }$${\displaystyle \langle G,S\rangle }$

${\displaystyle f^{-1}[A]\in V}$すべての について。${\displaystyle A\in W}$

フレームのインデックス付きセットの非結合和集合はフレームであり、 はの非結合和集合、はの和集合、 は ${\displaystyle \mathbf {F} _{i}=\langle F_{i},R_{i},V_{i}\rangle }$${\displaystyle i\in I}$${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$${\displaystyle F}$${\displaystyle \{F_{i}\mid i\in I\}}$${\displaystyle R}$${\displaystyle \{R_{i}\mid i\in I\}}$

${\displaystyle V=\{A\subseteq F\mid \forall i\in I\,(A\cap F_{i}\in V_{i})\}.}$

フレームの洗練とは、以下のように定義される洗練されたフレームである。同値関係を考える。${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$${\displaystyle \mathbf {G} =\langle G,S,W\rangle }$

${\displaystyle x\sim y\iff \forall A\in V\,(x\in A\Leftrightarrow y\in A),}$

を の同値類の集合とする。すると、 ${\displaystyle G=F/{\sim }}$${\displaystyle \sim }$

${\displaystyle \langle x/{\sim },y/{\sim }\rangle \in S\iff \forall A\in V\,(x\in \Box A\Rightarrow y\in A),}$

${\displaystyle A/{\sim }\in W\iff A\in V.}$

クリプキ フレームとは異なり、すべての通常の様相論理は、一般フレームのクラスに関して完全です。これは、 がクリプキ モデルのクラスに関して完全であるという事実の結果です。 は置換に対して閉じているため、 によって誘導される一般フレームは-フレームです。さらに、すべての論理は単一の記述フレームに関して完全です。実際、はその標準モデルに関して完全であり、標準モデルによって誘導される一般フレーム (の標準フレームと呼ばれる) は記述的です。 ${\displaystyle L}$${\displaystyle L}$${\displaystyle \langle F,R,{\Vdash }\rangle }$${\displaystyle L}$${\displaystyle \langle F,R,{\Vdash }\rangle }$${\displaystyle L}$${\displaystyle L}$${\displaystyle L}$${\displaystyle L}$

一般フレームは様相代数と密接な関係があります。を一般フレームとします。集合 はブール演算で閉じているため、これは冪集合ブール代数の部分代数です。また、追加の単項演算 も実行します。組み合わせた構造は様相代数であり、の双対代数と呼ばれ、 と表記されます。 ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$${\displaystyle V}$ ${\displaystyle \langle {\mathcal {P}}(F),\cap ,\cup ,-\rangle }$${\displaystyle \Box }$${\displaystyle \langle V,\cap ,\cup ,-,\Box \rangle }$${\displaystyle \mathbf {F} }$${\displaystyle \mathbf {F} ^{+}}$

反対に、任意の様相代数 への双対フレームを 構築することができます。ブール代数 には、のすべての超フィルタの集合を基礎とするストーン空間 があります。の許容値集合は の閉開集合から構成され、アクセス可能性関係は次のように定義されます。 ${\displaystyle \mathbf {A} _{+}=\langle F,R,V\rangle }$${\displaystyle \mathbf {A} =\langle A,\wedge ,\vee ,-,\Box \rangle }$${\displaystyle \langle A,\wedge ,\vee ,-\rangle }$${\displaystyle F}$${\displaystyle \mathbf {A} }$${\displaystyle V}$${\displaystyle \mathbf {A} _{+}}$${\displaystyle F}$${\displaystyle R}$

${\displaystyle x\,R\,y\iff \forall a\in A\,(\Box a\in x\Rightarrow a\in y)}$

すべてのウルトラフィルターおよび。 ${\displaystyle x}$${\displaystyle y}$

フレームとその双対は同じ公式を検証します。したがって、一般的なフレーム意味論と代数意味論はある意味で同等です。任意の様相代数の二重双対は、それ自体と同型です。これは一般にフレームの二重双対には当てはまりません。すべての代数の双対は記述的だからです。実際、フレームが記述的であるのは、フレームがその二重双対と同型である場合のみです。 ${\displaystyle (\mathbf {A} _{+})^{+}}$${\displaystyle \mathbf {A} }$${\displaystyle \mathbf {F} }$${\displaystyle (\mathbf {F} ^{+})_{+}}$

また、一方では p 射の双対を定義し、他方では様相代数準同型を定義することも可能である。このようにして、演算子とが、一般フレームのカテゴリと様相代数のカテゴリの間の反変関数のペアになる。これらの関数は、記述フレームのカテゴリと様相代数の間の双対性( Bjarni JónssonとAlfred TarskiにちなんでJónsson–Tarski 双対性と呼ばれる)を提供する。これは、複素代数と関係構造上の集合体の間のより一般的な双対性の特殊なケースである。 ${\displaystyle (\cdot )^{+}}$${\displaystyle (\cdot )_{+}}$

直観主義論理と中間論理のフレーム意味論は、様相論理の意味論と並行して展開することができる。直観主義一般フレームは、 の半順序である3 つの であり、は の上側部分集合（錐）の集合であり、空集合を含み、 の下で閉じている。 ${\displaystyle \langle F,\leq ,V\rangle }$${\displaystyle \leq }$${\displaystyle F}$${\displaystyle V}$${\displaystyle F}$

• 交差と結合、
• 操作。${\displaystyle A\to B=\Box (-A\cup B)}$

妥当性やその他の概念は、様相フレームと同様に導入されるが、許容可能な評価集合の弱い閉包特性に対応するためにいくつかの変更が必要である。特に、直観主義フレームは ${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$

• タイト、意味する場合、${\displaystyle \forall A\in V\,(x\in A\Leftrightarrow y\in A)}$${\displaystyle x\leq y}$
• 有限交差特性を持つ のすべての部分集合に空でない交差がある場合、はコンパクトです。${\displaystyle V\cup \{F-A\mid A\in V\}}$

厳密な直観主義のフレームは自動的に微分化され、洗練されます。

直観主義フレームの双対はヘイティング代数である。ヘイティング代数の双対は直観主義フレーム であり、 はのすべての素数フィルタの集合であり、順序はの包含であり、の形式の すべての部分集合から構成される。${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$ ${\displaystyle \mathbf {F} ^{+}=\langle V,\cap ,\cup ,\to ,\emptyset \rangle }$${\displaystyle \mathbf {A} =\langle A,\wedge ,\vee ,\to ,0\rangle }$${\displaystyle \mathbf {A} _{+}=\langle F,\leq ,V\rangle }$${\displaystyle F}$${\displaystyle \mathbf {A} }$${\displaystyle \leq }$${\displaystyle V}$${\displaystyle F}$

${\displaystyle \{x\in F\mid a\in x\},}$

ここで。様相の場合と同様に、と は反変関数のペアであり、これにより Heyting 代数のカテゴリは記述的直観主義フレームのカテゴリと双対的に同値になります。 ${\displaystyle a\in A}$${\displaystyle (\cdot )^{+}}$${\displaystyle (\cdot )_{+}}$

直観主義的な一般フレームを推移的再帰的様相フレームから構築することは可能であり、その逆も可能です。 様相コンパニオンを参照してください。

• 近隣セマンティクス

• Alexander Chagrov と Michael Zakharyaschev、「Modal Logic」、Oxford Logic Guides の第 35 巻、Oxford University Press、1997 年。
• Patrick Blackburn、Maarten de Rijke、Yde Venema、「Modal Logic」、Cambridge Tracts in Theoretical Computer Science の第 53 巻、Cambridge University Press、2001 年。