形式的証明可能性と矛盾の関係の補題
タイトルの補題名は一般的なものではないmrsekut.icon
補題
いかなる論理式の集合$ \Gammaと論理式$ Aについても、以下が成り立つ
$ \Gamma\vdash A\Leftrightarrow \Gamma\cup\{\lnot A\}は構文論的に矛盾する
簡潔に書くなら
$ \Gamma\vdash\varphi\Leftrightarrow\Gamma\{\lnot\varphi\}\vdash\bot
証明
本当はどの演繹体系を使うかを指定しないといけないがmrsekut.icon $ \Rightarrow側
仮定より$ \Gamma=\{\phi_1,\cdots,\phi_{n-1}\}によって、$ \varphiが導けるとする
$ 0: \phi_1
$ \cdots
$ n-1:\phi_{n-1}
$ n: \varphi
ここに、2つを加える
$ n+1: \lnot\varphi(仮定)
$ n+2:\bot ($ n,n+1$ \lnot E)
よって、$ \Gamma\{\lnot\varphi\}\vdash\botの形式的証明が得られた
$ \Leftarrow側
仮定の$ \Gamma\{\lnot\varphi\}\vdash\botを以下のように表すとする
$ 0:\phi_1
$ \cdots
$ m:\lnot\varphi
$ \cdots
$ n-1: \phi_{n-1}
$ n: \bot
ここに、2つを加える
$ n+1:\lnot\lnot\varphi ($ m,\lnot I)
$ n+2:\varphi ($ n+1$ \lnot\lnot E)
よって、$ \Gamma\vdash\varphiの証明が得られた
参考