論理学に関する記号とその意味

\mathrm{FVar}(\varphi): 論理式\varphiに含まれる自由変数の集合

\mathrm{BVar}(\varphi):↑の束縛変数版

\varphi[t/x_i]:論理式\varphiの自由変数x_iに、項tを代入したもの

t[u/x_i]: 項tの変数x_iに、項uを代入したもの

ref シークエント計算

構文論的帰結には\vdashを使う

A_1,A_2,\cdots,A_n\vdash C

A_1,A_2,\cdots,A_nを仮定してCを導く

ざっくりいうと

\vdash\varphiは、「\varphiが証明できる」ということ

\Gamma\vdash\varphi

\varphiが\Gammaから証明可能であることをこのように表記する

\Gammaを論理式の集合、\varphiを論理式

\Gammaが有限集合\{\gamma_1,\cdots,\gamma_n\}のときは、\gamma_1,\cdots,\gamma_n\vdash\varphiとも書く

\Gammaが空集合のときは、\vdash\varphiとも書く

上のやつとほぼ同じ

わかりやすく書くなら(\GammaとA)\vdash C

\Gammaは集合で、A,Cは式であることに注意する

\Gammaに含まれる全ての仮定と、Aを仮定することで、Cが演繹できる

ということを言っている

演繹定理に出てくる

\Gammaから導かれるものが空集合

意味論的帰結は\vDashを使う

A_1,A_2,\cdots,A_nが全て真になるような真理値割り当てのもとで、Cも真になる

逆に言えば、A_1,A_2,\cdots,A_nが全て真で、Cが偽になるような真理値割り当ては存在しない

ざっくりいうと、

\vDash\varphiは、「\varphiが正しい」ということ

トートロジーは\vDash\varphi

\Gamma\vDash\varphi

上のやつの集合版

\Gammaに属する論理式をすべて真にするような、どのような真理値割当に対しても\varphiが真となるとき\Gamma\vDash\varphiと書く

もうちょいスマートに言うと

\Gammaを充足する任意の真理値割り当ての元で、\varphiも真になる

\Gammaは論理式の集合

\varphiは命題論理式

ref p.4 定義1.6

\mathcal{M}\vDash\Gamma

左辺がモデルなのがポイント

上の\Gamma\vDash\varphiと似て非なるものであることに注意

\mathcal{M}は言語Lに対応するストラクチャ

\Gammaは言語Lの閉論理式の集合

論理式\forall\varphi\in\Gammaが\mathrm{eval}_\mathcal{M}(\varphi)=\topのとき\mathcal{M}\vDash\Gammaと書く

このとき、\mathcal{M}のことを\Gammaのモデルという

言語Lと対象領域Mが、記号\mathcal{M}\vDash\Gammaに現れないのが、ややこしさを増している原因になっている気がする

あと、下図をみても分かる通り\Gammaと\mathcal{M}の位置が離れているのもムズイ感が増す