Unknowable

不完全性定理についてのゲーデルの証明

不動点

f = Function[{x}, x[Hold[x]]];

次のように書いてもいい
f=Function[#[Hold[#]]];
f=#[Hold[#]]&;
しかしf[x_]:=x[Hold[x]]ではない

f[f]

ReleaseHold[f[f]]

f[f] === ReleaseHold[f[f]]

ゲーデルの定理

エピメニデスのパラドックス：「この文は偽である」
ゲーデルの定理：「この命題は証明できない」（真なのに証明できない命題がある）

g = Function[isUnprovable[valueOf[#[Hold[#]]]]];

g[g]

g[g] === ReleaseHold[First[First[g[g]]]]

停止問題の解決不可能性についてのチューリングの証明

ラッセルのパラドックス：
	自分の髭を剃らない村中すべての男の髭を剃る床屋
チューリングの定理：
	任意のプログラムが停止するかどうかを判断できるようなアルゴリズムは存在しない

haltsQがFalseを返すつまり停止しないと判断する場合

turing = 
        Function[{x}, Function[{haltsQ}, Function[{z}, 
                  If[haltsQ[z], ReleaseHold[z], False]][
                Print[x[Hold[x]]]]][Function[{sExp}, False]]];

turing[turing]

haltsQがTrueを返すつまり停止すると判断する場合

turing = 
        Function[{x}, Function[{haltsQ}, Function[{z}, 
                  If[haltsQ[z], ReleaseHold[z], False]][x[Hold[x]]]][
            Function[{sExp}, True]]];

turing[turing]

式がエレガントであることを証明できないというチャイティンの証明

準備

print = Function[{x}, Print[x];  x];

size[x_] := StringLength[ToString[x]]

パラドックスなし

ex = 
        Function[{}, 
          fas = Function[{n}, 
              Switch[n, 
1, 
                Hold[isElegant[
                    x]], 
2, {}, 
3, 
                Hold[isElegant[yyy]], 
_, 
                stop]]; 
repeat = 
            Function[{n}, 
              With[{theorem = print[ReleaseHold[fas[n]]]}, 
                If[{} === theorem, repeat[n + 1], 
                  If[stop === theorem, fasHasStopped, 
                    If[isElegant === theorem[[0]], 
                      If[print[size[theorem[[1]]]] > print[size[ex]], 
                        theorem[[1]], repeat[n + 1]], 
                      repeat[n + 1]]]]]]; 
repeat[
            1]];

ex[]

ベリーのパラドックス

ex = 
        Function[{}, 
          fas = Function[{n}, 
              Switch[n, 
1, 
                Hold[isElegant[
                    x]], 
2, {}, 
3, 
                Hold[isElegant[yyy]], 
4, 
                Hold[isElegant[10^535]], 
_, 
                stop]]; 
repeat = 
            Function[{n}, 
              With[{theorem = print[ReleaseHold[fas[n]]]}, 
                If[{} === theorem, repeat[n + 1], 
                  If[stop === theorem, fasHasStopped, 
                    If[isElegant === theorem[[0]], 
                      If[print[size[theorem[[1]]]] > print[size[ex]], 
                        theorem[[1]], repeat[n + 1]], 
                      repeat[n + 1]]]]]]; 
repeat[
            1]];

ex[]