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

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

「不完全性定理(7) - エレファント・ビジュアライザー調査記録」の計算が間違っていたので書き直します。「コード化」と「逆コード化」を導入します。

$L$ を論理式全体の集合とします。 $\mathbb{N} \to L$ を自然数全体から論理式全体への写像全体の集合とします。
$\mathbb{N} \to L$ の元を「コード化」して自然数で表すことができるとします。 $\mathbb{N} \to L$ の元を「コード化」した自然数全体の集合を $C(\mathbb{N} \to L)$ で表します。「コード化」する写像を $c: (\mathbb{N} \to L) \to C(\mathbb{N} \to L)$ とおきます。
$C(\mathbb{N} \to L)$ の元を「逆コード化」して $\mathbb{N} \to L$ の元に戻すことができるとします。「逆コード化」する写像を $d: C(\mathbb{N} \to L) \to (\mathbb{N} \to L)$ とおきます。 $d \circ c$ は恒等写像とします。
$p: (\mathbb{N} \to L) \to (\mathbb{N} \to L)$ を、 $p(r)$ は「 $r$ が証明できる」ことを表すものとします。
$n: (\mathbb{N} \to L) \to (\mathbb{N} \to L)$ を、 $n(r)$ は $r$ の否定を表すものとします。
$g: C(\mathbb{N} \to L) \to C(\mathbb{N} \to L) \to (\mathbb{N} \to L)$ を $g(f)(e) = p(d(f)(e))$ とおきます。
$h: C(\mathbb{N} \to L) \to (\mathbb{N} \to L)$ を $h(v) = n(g(v)(v))$ とおきます。
$k \in C(\mathbb{N} \to L)$ を $k = h(c(h))$ とおきます。

このとき
$\begin{eqnarray*} k & = & h(c(h)) \\ & = & n(g(c(h))(c(h))) \\ & = & n(p(d(c(h))(c(h)))) \\ & = & n(p(h(c(h)))) \\ & = & n(p(k)) \\ \end{eqnarray*}$
となって $k = n(p(k))$ が成り立ちます。

これをラムダ計算の形に書き直します。

$\mapsto$ をラムダ計算のラムダ抽象(右結合)、 $\ll$ をラムダ計算の関数適用とします。 $\gg$ を $\ll$ の左右の演算数を入れ替えたもの( $x \gg y = y \ll x$ )とします。すなわち $y \gg (x \mapsto e)$ は式 $e$ の自由変数 $x$ を式 $y$ で置き換えたものとなります。 $\gg$ は左結合とします。
$c$ と $d$ はあらかじめ定義されていて、 $c \gg d$ は恒等写像とします。
$p$ と $n$ はあらかじめ定義されているとします。

このとき

$g = f \mapsto e \mapsto (e \gg (f \gg d) \gg p))$
$h = v \mapsto (v \gg (v \gg g) \gg n)$
$k = h \gg c \gg h$

とおくと
$\begin{eqnarray*} k & = & h \gg c \gg h \\ & = & h \gg c \gg (h \gg c \gg g) \gg n \\ & = & h \gg c \gg (h \gg c \gg d) \gg p \gg n \\ & = & h \gg c \gg h \gg p \gg n \\ & = & k \gg p \gg n \\ \end{eqnarray*}$
となって $k = k \gg p \gg n$ が成り立ちます。