巨大数探索スレッド13
■ このスレッドは過去ログ倉庫に格納されています
https://twitter.com/wota1969?t=1&;cn=ZmxleGlibGVfcmVjcw%3D%3D&refsrc=email&iid=7ee5dd3e1aad40d9a574c9f18d8e62a1&uid=525178774&nid=244+272699405 俺的文明レベルの定義
文明のレベルはビジービーバー関数の値をどこまで求められるかで測られる。
現在の人類の文明レベルは4 囲碁、チェス、将棋のプログラムで一気にトップに出た Google に、
絶大なコンピュターパワーでビジービーバー関数の計算にチャレンジしてほしい GIMPSみたいに分散コンピューティングしたいけれどあまりにも知名度が 名前がよくない
いっそ社畜関数って名前にしてしまえばもっと共感を呼ぶ 計算量がそのまんまビジービーバー関数レベルで増えていってやばい。
指数関数レベルの増え方とは次元が違う・・・と思ったけどほんとにそうだろうだろうか？ 停止するプログラムをすべて最後まで走らせてその中で最大の値を求める。
これは本当に最後まで走らせる必要があるわけではない、
どこまで計算効率を上げられるか
停止しないプログラムは停止しないという判定をしなければならない。
限定的に停止性を判定するアルゴリズムは存在するものの、それをどこまで簡単にできるか？
またそのプログラムを開発するプログラムはもっと複雑になるのではないか？
停止性を判定するプログラムはオラクルで与えられてもいい、つまり適当に作ったプログラムが
たまたまそうなっていたとしてもいい、ではそれがほんとうに停止性を判定するプログラムであると
判定するプログラムは？
停止性を判定するプログラムであると判定するプログラムであると判定するプログラムは？
これもうわかんねえな >>13
普通にゲーデルの不完全性定理を停止問題として言い換えられるのぐらい知ってて言ってるよね？。 BB(100)とかは無理だろうけど、BB(5)とかBB(6)くらいなら、
Googleが頑張ればそのうちなんとか、とか思わないでもない 実際に求める必要なんてないと思うが
グラハム数だって計算しようなんてヤツはいない >>14あくまで限定的な停止性判定のアルゴリズムの話なので。
たとえば4状態のプログラムは有限個しか存在しないので、究極最初からプログラムの中に
それぞれの入力されたプログラムに対する答えを用意しとけば4状態の停止性を判定する
プログラムとなります。
と書いて思ったけどこんなのでもアルゴリズムと言っていいのか？ プログラムとは言えるけど 計算可能レベルの追究が結果的にビジービーバー関数の値を求めることにもなるだろう。
逆も然りだが、こちらからはけっこう難解 実際に求めると言うのは、当然10進数で求めるという意味ではなくて、
優勝マシンを決定すること
その一般的なアルゴリズムはないけど、小さいnに対しては決定できても
おかしくはない 巨大数ベイクオフ大会もある意味BB(512)の値を追求する大会ですし 前スレでビジービーバー関数の全域性うんぬん言ってたやつに致命的な間違いを見つけた。
ω矛盾の定義がおかしい。∃n∈(自然数)(Q(n))が証明可能なのに
Q(0),Q(1),Q(2),...がいずれも証明不能であることをω矛盾の定義といってたが、
これだとペアノ算術に例えば定数記号aを加えただけの拡張でも、
a = a から ∃n (a = n)が導出できる一方で、a = 0,a = 1,a = 2,... のいずれも証明不能で、
ω矛盾になる。しかし、これにa = 0という仮定を加えても無矛盾だから、
超準モデルになるとは限らない。
間違いの源はおそらく日本語版wikipediaだ。
"ω矛盾とは、自然数 n によって定まる論理式 Q(n) が存在して、次を満たすことをいう。
Q(0), Q(1), Q(2), …が全て証明可能であるが、「∃n： ¬Q(n) 」も証明可能である"
この記述は正しい。問題があるのはその下の、
"公理系が無矛盾であれば、対偶を取る事により、ω矛盾の概念が次と同値である事を示せる：
「∃n： Q(n) 」が証明可能であるが、Q(0), Q(1), Q(2), … のいずれも証明可能ではない。"
というところだ。最初の記述は「Q(0),Q(1),Q(2),...が証明可能で、かつ∃n(¬Q(n))も証明可能」
と言い換えられる。すると、実はAならばBの形になってないから、そもそも"対偶を取る"のは変だ。
英語版wikipediaには下の記述に該当する文は無い。
同値でないことも簡単に確認できる。ペアノ算術に定数記号aを加えただけの拡張は、
∃n(a = n)が証明可能で、a = 0, a = 1, ...が証明不能なことから下の記述を満たすが、
∃n(¬(a ≠ n))が証明可能な一方、a ≠ 0, a ≠ 1, ...は証明不能だから、上の記述を満たさない。
よって2つの記述は同値でない。
だから、前スレのあの証明では、「ビジービーバー関数の出力が超準的自然数になる」ことは
証明できていない、と言える。
あー、すっきりした まぁでも、「ビジービーバー関数の出力が超準的自然数になる」、すなわち
BB(x)をビジービーバー関数として、
「十分大きな自然数Mについて、0 < BB(M), 1 < BB(M), 2 < BB(M), ...が証明可能」
は証明できてないけど、もっと弱い主張である※ならば簡単に証明できる。
(∀n(n < BB(M))と、0 < BB(M), 1 < BB(M), ...は異なる。∀n (n < BB(M))からは、
例えばBB(M) + 1 < BB(M) を導出できるので明らかに矛盾)
※: 任意の無矛盾かつ帰納的公理化可能な公理について、ある自然数Mが存在して、
任意のn ∈ {0,1,2,...}について公理に n < BB(M) という式を加えてもなお無矛盾
やや分かりにくいけど、公理に0 < BB(M)とか1 < BB(M)とか 2 < BB(M)をいくら加えても
そこから矛盾が導出できない、ということ。ビジービーバー関数を扱える公理じゃないと
いけないので、多分自然数論を含むだろう。 証明: 背理法による。どんなに大きな自然数Mに対しても、n < BB(M)を仮定すると矛盾が
導出できるような n ∈ {0,1,2,...}が存在すると仮定する。
公理が帰納的公理化可能なので、以下のような計算機械を構成すれば、必ず停止する
k = 0 とする
親プロセス:
(1).子プロセスに k < BB(M)を与えて起動する
(2).子プロセスが1つでも停止したら(3)へ
そうでなければ k を 1 増やして(1)へ戻る
子プロセス:
k < BB(M)が与えられたら公理 + (k < BB(M))から
矛盾の導出を試みて、矛盾を導出したらkを出力して停止
また、親プロセスが停止したら停止
すべてのプロセスは並行して行われる
この計算機械の出力する値を N とすると、N < BB(M)から矛盾を導出したので
N ≧ BB(M)を導出でき、状態数M以下のチューリングマシンをエミュレートして
N個を超える1を出力した時点でそのチューリングマシンは停止しないと判定できる。
どんなに大きな自然数Mに対してもこのことが言えるので、
任意の停止性問題を解ける計算機械が構成できることになり矛盾する。
よって背理法より※が示された。 ※からは面白いことが分かる。
例えば、いかに大きなn∈{0,1,2,...}についてもn < BB(M)の仮定と矛盾しないということは
ある程度大きなMについてBB(M)に意味のある上限を導出できないことを意味する。
上限 m∈{0,1,2,...} が導出できるなら、m < BB(M)の仮定を加えると矛盾し、※に反するから。
(ここでいう意味のない上限とは、BB(M) < BB(M) + 1など)
ある程度大きなというのがどれくらいかは公理によるが、例えばZFCで100とすると
BB(100)の上限がふぃっしゅ数ver6ぐらい、とか、H(ψ(Ω_ω))である、といった
何かしら計算可能なもので表せると証明されることはありえない、ということになる。
あとは、"公理が無矛盾 ⇒ 公理 + (n < BB(M)) が無矛盾"は示した通りだが
逆は明らかなので公理と公理 + (n < BB(M))は無矛盾性同値でもある。
なんだか、まるでBB(M)は連続体濃度みたいな感じがする。
連続体濃度cも、ZFC + (アレフ1 < c) とか ZFC + (アレフ2 < c),...にしたって無矛盾だし、
cは存在するし一定の濃度でもあるはずだけど、可算無限との間にいくつの濃度の異なる集合が
あるのか決まらない、といったような。
何をもって一意に定まるとするのかは、もはや哲学の問題だね。 いまだにビジービーバーみたいな小さな関数で思考が止まってるのか グラハム数が指数の塔で表現出来なくても
ちゃんと大きさが見積もれる 前スレの「フワフワした感じがすっきりしないんじゃないか？」を「大きさを見積もることができない」
と言っていると勘違いされた可能性はどうだろう >>26
「どんなに大きな自然数Mに対しても、n < BB(M)を仮定すると矛盾が
導出できるような n ∈ {0,1,2,...}が存在する」
としたら、「1をn個出力するまでチューリングマシンを走らせる」とするだけで
停止性問題が解決してしまうので、そういうnが存在しないということが
停止性問題と同値であることは自明 >>31
小さな数しか作れないものは否定されてもしょうがない ■ このスレッドは過去ログ倉庫に格納されています
