極大無矛盾なヘンキン性
$ \Gamma^+と表記する
このノートではもっと言語$ Lに対する言及が必要
時間がなくて説明を端折ってしまったmrsekut.icon
『学んでみよう！記号論理』.iconの15章や、授業のpdfを参考
memo
『学んでみよう！記号論理』.iconでは、$ Lから作られる全ての閉論理式の集合を$ \mathscr{CF}_Lとし
モデルを持った閉論理式の集合を$ \Gammaとしている
$ \Gamma^\astの性質
$ \Gamma\subset\Gamma^\ast
$ \Gamma^\astは$ L^\astのヘンキン性 $ \Gamma^+の性質
$ \Gamma\subset\Gamma^+
$ \Gamma^+は$ L^\astのヘンキン性 以下のステップで$ \Gammaを拡張する
$ \Gamma^\astを作る
同時に拡大した言語$ L^\astを作る
$ \Gamma^+を作る
$ \Gamma^\astを作る
ステップ
言語$ Lに定数記号を追加して$ L^\ast=L\cup Cにする
$ Cは定数記号の集合
言語$ Lに定数記号を追加して$ L^\astにする
定数記号を加えただけでは矛盾は生じない ref 以下の補題6.9
$ \Gamma^+を作る
$ \Gamma^\astを無矛盾に保ちつつ、$ \mathscr{CF}_Lの論理式を追加していく
補題
$ \Deltaを$ Lで極大無矛盾なヘンキン性とする
このとき$ \mathrm{FVar}(\rho)\subset\{x\}を満たす$ Lの論理式$ \rhoについて以下が成り立つ
$ (\forall x\rho)\in\Delta$ \Leftrightarrow
全ての$ Lの閉項$ t
について$ \rho[t/x]\in\Delta
$ (\exist x\rho)\in\Delta$ \Leftrightarrow
あるの$ Lの閉項$ t
について$ \rho[t/x]\in\Delta
補題6.8 ref 授業のPDF p.32 補題6.8
$ \Theta\vdash\psi[c/x] を表す導出図 $ A が存在するとき
$ Aに現れる定数記号 $ c を
$ Aにも ψ にも 現れない変数記号 $ zで
いっせいに置き換えると
$ \Theta\vdash\psi[z/x] を表す導出図が得られる
補足
$ \Thetaは論理式の集合
$ \psiは論理式
$ cは$ \Thetaに属する論理式にも、$ \psiにも現れない定数記号
補題 6.9 ref 授業のPDF p.32 補題6.9
$ \Delta が無矛盾ならば，
$ \Delta \cup \{\exist x \varphi \rightarrow \phi[e/x]\} も無矛盾である.
補足
$ \Deltaを論理式の集合
$ \phi を$ \mathrm{FVar}(\phi) \subset \{x\} をみたす論理式
$ e を $ \Delta に属する論理式にも $ \phiにも出現しない定数記号