Gödelの第2不完全性定理の証明旧版
メモ
古いし，多分間違っている．
目標
以下を示す．
Gödelの第2不完全性定理: 体系$ \mathscr{S}がω無矛盾であるなら，$ \mathscr{S}が無矛盾であるということを意味する$ \mathscr{S}の論理式$ \mathrm{Con}(\mathscr{S})は$ \mathscr{S}で証明可能ではない．
参考文献
論理と計算のしくみ(本)
TODO　
$ \mathrm{Formula} \lbrack \overline{x} \rbrackが表現可能であることの証明
$ \mathrm{IT}_1が$ \mathscr{S}で証明可能であることの証明
爆発律に関して
体系の無矛盾性を次のように定める
$ \mathscr{S}において$ Aと$ \lnot Aが両方証明可能な論理式$ Aが存在しないとき，体系は無矛盾
逆にそのような$ Aが存在するなら$ \mathscr{S}は矛盾している
ところで，$ \mathscr{S}に爆発律が備わっているなら，$ A \land \lnot Aから任意の論理式$ Bが証明出来る．
すなわち，$ A \land \lnot A \vdash_{\mathscr{S}} B
逆に言えば，
$ \mathscr{S}に爆発律が備わっていながら証明できないような論理式$ Pが存在するなら，少なくとも矛盾はしていないことがわかる．
記号の準備
$ xを自然数とする．
$ xが$ \mathscr{S}の論理式の符号であることを表現する論理式を$ \mathrm{Formula} \lbrack \overline{x} \rbrackとする．
この論理式が存在することの証明は省略する．
$ xが$ \mathscr{S}で証明可能な論理式の符号であることを表現する論理式$ \mathrm{Provable} \lbrack \overline{x} \rbrackとする．
詳しくはGödelの第1不完全性定理参照．
体系$ \mathscr{S}が矛盾していないことを$ \mathrm{Con}(\mathscr{S})と表すとする，
上記より，$ \mathscr{S}には爆発律が備わっていると仮定すれば，
$ \mathrm{Con}(\mathscr{S}) = \exists \bar{x}.( \mathrm{Formula} \lbrack \overline{x} \rbrack \land \lnot \mathrm{Provable} \lbrack \overline{x} \rbrack)
が成り立つ．
Gödelの第1不完全性定理の形式化
厳密には違うが，Gödelの第1不完全性定理は下記のとおりである．
Gödelの第一不完全性定理: 無矛盾な体系$ \mathscr{S}で，$ Gも$ \lnot Gも証明出来ないような文$ Gを構成可能．
ω無矛盾性を取っ払った．
この$ Gについて，次の事実が存在する．
補題1: $ Gが証明可能$ \iff$ \lnot \mathrm{Provable} \lbrack \overline{ \ulcorner G \urcorner } \rbrackが証明可能
Gödelの第1不完全性定理#63beade913a1580000123604
この定理を体系$ \mathscr{S}の中で表現する論理式$ \mathrm{IT}_1とは
$ \mathrm{IT}_1 = \mathrm{Con}(\mathscr{S}) \to \exists G. \lnot \mathrm{Provable} \lbrack \overline{\ulcorner G \urcorner} \rbrack
今，$ \mathrm{IT}_1が$ \mathscr{S}自身の中で証明可能だったとする．
TODO: 証明
Gödelの第2不完全性定理
$ \mathrm{Con}(\mathscr{S})が$ \mathscr{S}で証明可能であったとする．
$ \mathrm{IT}_1より，$ \exists G.\lnot \mathrm{Provable} \lbrack \overline{\ulcorner G \urcorner} \rbrackが$ \mathscr{S}で証明可能である．
$ \mathscr{S}のω無矛盾性より，その条件を満たす$ G_0が存在する．
すなわち，$ \lnot \mathrm{Provable} \lbrack \overline{\ulcorner G_0 \urcorner} \rbrackは$ \mathscr{S}で証明可能
また補題1より，$ G_0が$ \mathscr{S}で証明可能である．
後はGödelの第1不完全性定理#63beabde13a15800001235f9と同じように議論することが出来る．
すなわち，
$ G_0の証明の符号を表す自然数$ y_0が存在して，
$ \mathrm{proof}(\ulcorner G_0 \urcorner,y_0) = 0が成り立つ．
表現可能性より，$ \mathrm{Proof} \lbrack \overline{\ulcorner G_0 \urcorner},\overline{y_0},\overline{0} \rbrackが$ \mathscr{S}で証明可能
定義より，$ \mathrm{Provable} \lbrack \overline{\ulcorner G_0 \urcorner}\rbrackも$ \mathscr{S}で証明可能
$ \mathscr{S}は無矛盾であるので，$ \mathrm{Provable} \lbrack \overline{\ulcorner G_0 \urcorner}\rbrackも$ \lnot \mathrm{Provable} \lbrack \overline{\ulcorner G_0 \urcorner} \rbrackも$ \mathscr{S}で証明可能であることは無矛盾性の前提に反する．
したがって，$ \mathrm{Con}(\mathscr{S})は$ \mathscr{S}で証明可能ではない．
纏めると，
Gödelの第2不完全性定理: 体系$ \mathscr{S}がω無矛盾であるなら，$ \mathscr{S}が無矛盾であるということを意味する$ \mathscr{S}の論理式$ \mathrm{Con}(\mathscr{S})は$ \mathscr{S}で証明可能ではない．