不完全性定理(13) - 非専門的シンギュラリティー研究所

プログラミング言語版不完全性定理(8)

第2不完全性定理の証明を書き直していきます。

証明関数

論理式と証明図をプログラミング言語のコードとして表すことができるシステムについて考えます。

このシステムで論理式が証明できるかどうかを調べるプログラミング言語の関数 $\mathcal{P}$ があるとします。 $\mathcal{P}$ に入力された論理式のコード $x$ に対して

(P1) $\mathcal{P}(x)$ は終了して「成功」を返す
(P2) $\mathcal{P}(x)$ は終了して「失敗」を返す
(P3) それ以外

の場合があるとします。(P1) のとき $\mathcal{P} \vdash x$ と表すことにします。(P1) 以外のとき $\mathcal{P} \not \vdash x$ と表すことにします。

論理式の形式

まず『数学基礎論 (ちくま学芸文庫)』の記述に合わせて論理式のコードを論理式の形式で記述します。

(1): を「論理式が証明できる」ことを表す論理式のコードとします。以下が成り立つとします。
- (1-1): $\mathcal{P} \vdash x \implies \mathrm{Prov}(x)$
- (1-2): $\mathcal{P} \vdash \mathrm{Prov}(x) \implies x$
(2): $\bot$ を矛盾を表す一つの論理式のコードとします。
(3): $\mathrm{Consis} \iff \lnot \mathrm{Prov}(\bot)$ と定義します。
(4): 第1不完全性定理の主張はとなります。ここで
- (4-1): $k \iff \lnot \mathrm{Prov}(k)$ ( $k$ は第1不完全性定理の証明に現れた $k$ )
(5): が成り立ちます。なぜなら
- (5-1): (1-2) から $\mathcal{P} \vdash \mathrm{Prov}(k) \implies k$ が成り立ちます。
- (5-2): (5-1) と (4-1) から $\mathcal{P} \vdash \mathrm{Prov}(k) \implies \lnot \mathrm{Prov}(k)$ が成り立ちます。
- (5-3): (5-2) から $\mathcal{P} \vdash \mathrm{Prov}(k) \implies \bot$ が成り立ちます。
- (5-4): (5-3) と (1-1) から $\mathcal{P} \vdash \mathrm{Prov}(k) \implies \mathrm{Prov}(\bot)$ が成り立ちます。
- (5-5): (5-4) から $\mathcal{P} \vdash \lnot \mathrm{Prov}(\bot) \implies \lnot \mathrm{Prov}(k)$ が成り立ちます。
- (5-6): (5-5) と (3) から (5) が成り立ちます。
(6): (5) と (1-1) から $\mathcal{P} \vdash \mathrm{Consis} \implies \mathrm{Prov}(\lnot \mathrm{Prov}(k))$ が成り立ちます。
(7): (6) と (4-1) から $\mathcal{P} \vdash \mathrm{Consis} \implies \mathrm{Prov}(k)$ が成り立ちます。
(8): (5) と (7) から $\mathcal{P} \vdash \mathrm{Consis} \implies \bot$ が成り立ちます。
(9): (8) から $\mathcal{P} \vdash \mathrm{Consis}$ ならば $\mathcal{P} \vdash \bot$ が成り立ちます。
(10): (9) から $\mathcal{P} \not \vdash \bot$ ならば $\mathcal{P} \not \vdash \mathrm{Consis}$ が成り立ちます。よって $\mathcal{P}$ が無矛盾ならば $\mathcal{P}$ で $\mathrm{Consis}$ は証明できません。

関数の形式

次に「不完全性定理(10) - エレファント・ビジュアライザー調査記録」で書いたような関数の形式に書き直します。

(1): を「論理式が証明できる」ことを表す論理式のコードとします。以下が成り立つとします。
- (1-1): $\mathcal{P} \vdash x \to p(x)$
- (1-2): $\mathcal{P} \vdash p(x) \to x$
(2): $\mathbf{f}$ を矛盾を表す一つの論理式のコードとします。
(3): $\mathbf{c} = n(p(\mathbf{f}))$ と定義します。
(4): 第1不完全性定理の主張はとなります。ここで
- (4-1): $k = n(p(k))$ ( $k$ は第1不完全性定理の証明に現れた $k$ )
(5): が成り立ちます。なぜなら
- (5-1): (1-2) から $\mathcal{P} \vdash p(k) \to k$ が成り立ちます。
- (5-2): (5-1) と (4-1) から $\mathcal{P} \vdash p(k) \to n(p(k))$ が成り立ちます。
- (5-3): (5-2) から $\mathcal{P} \vdash p(k) \to \mathbf{f}$ が成り立ちます。
- (5-4): (5-3) と (1-1) から $\mathcal{P} \vdash p(k) \to p(\mathbf{f})$ が成り立ちます。
- (5-5): (5-4) から $\mathcal{P} \vdash n(p(\mathbf{f})) \to n(p(k))$ が成り立ちます。
- (5-6): (5-5) と (3) から (5) が成り立ちます。
(6): (5) と (1-1) から $\mathcal{P} \vdash \mathbf{c} \to p(n(p(k)))$ が成り立ちます。
(7): (6) と (4-1) から $\mathcal{P} \vdash \mathbf{c} \to p(k)$ が成り立ちます。
(8): (5) と (7) から $\mathcal{P} \vdash \mathbf{c} \to \mathbf{f}$ が成り立ちます。
(9): (8) から $\mathcal{P} \vdash \mathbf{c}$ ならば $\mathcal{P} \vdash \mathbf{f}$ が成り立ちます。
(10): (9) から $\mathcal{P} \not \vdash \mathbf{f}$ ならば $\mathcal{P} \not \vdash \mathbf{c}$ が成り立ちます。よって $\mathcal{P}$ が無矛盾ならば $\mathcal{P}$ で $\mathbf{c}$ は証明できません。