論理学に関する記号とその意味
$ \mathrm{FVar}(\varphi): 論理式$ \varphiに含まれる自由変数の集合 $ \mathrm{BVar}(\varphi):↑の束縛変数版 $ \varphi[t/x_i] :論理式$ \varphiの自由変数$ x_iに、項$ tを代入したもの
$ t[u/x_i] : 項$ tの変数$ x_iに、項$ uを代入したもの
$ 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が有限集合$ \{\gamma_1,\cdots,\gamma_n\}のときは、$ \gamma_1,\cdots,\gamma_n\vdash\varphiとも書く
$ \Gammaが空集合のときは、$ \vdash\varphiとも書く
$ \Gamma,A\vdash C
上のやつとほぼ同じ
わかりやすく書くなら$ (\GammaとA)\vdash C
$ \Gammaは集合で、$ A,Cは式であることに注意する
$ \Gammaに含まれる全ての仮定と、$ Aを仮定することで、$ Cが演繹できる ということを言っている
$ \Gamma\vdash A\rightarrow C
$ \Gamma\vdash
$ \Gammaから導かれるものが空集合
$ A_1,A_2,\cdots,A_nが全て真になるような真理値割り当てのもとで、$ Cも真になる
逆に言えば、$ A_1,A_2,\cdots,A_nが全て真で、$ Cが偽になるような真理値割り当ては存在しない
ざっくりいうと、
$ \vDash\varphiは、「$ \varphiが正しい」ということ
$ \Gamma\vDash\varphi
上のやつの集合版
$ \Gammaに属する論理式をすべて真にするような、どのような真理値割当に対しても$ \varphiが真となるとき$ \Gamma\vDash\varphiと書く
もうちょいスマートに言うと
$ \Gammaを充足する任意の真理値割り当ての元で、$ \varphiも真になる
$ \varphiは命題論理式
ref 『情報理論のための数理論理学』.icon p.4 定義1.6
$ \mathcal{M}\vDash\Gamma
上の$ \Gamma\vDash\varphiと似て非なるものであることに注意
$ \mathcal{M}は言語$ Lに対応するストラクチャ 論理式$ \forall\varphi\in\Gammaが$ \mathrm{eval}_\mathcal{M}(\varphi)=\topのとき$ \mathcal{M}\vDash\Gammaと書く
このとき、$ \mathcal{M}のことを$ \Gammaのモデルという 言語$ Lと対象領域$ Mが、記号$ \mathcal{M}\vDash\Gammaに現れないのが、ややこしさを増している原因になっている気がするmrsekut.icon
あと、下図をみても分かる通り$ \Gammaと$ \mathcal{M}の位置が離れているのもムズイ感が増す
https://gyazo.com/e4201abed9b588de8fd8f6f6b512f580
$ \Gamma\vDash