Edit Comment on 20091031-1

n[0] = "igaris";
m[0] = "こちらこそ、とても楽しい時間を過ごさせて頂きました。 ありがとうございました。 Σ_1健全性については、例えばゴールドバッハの予想が標準モデルで「真」だったとしても、ZFがΣ_1健全でないと、ZFでゴールドバッハの予想の反例の存在が証明される可能性がある、ということですよね。 「あるある」と言っても「ない」のは、T+￢Con(T)における「矛盾の証明」と同じですね。";
d[0] = "2009-10-31 22:49:16";
n[1] = "<a href="http://d.hatena.ne.jp/mushitoriseinen/">mushitoriseinen</a>";
m[1] = "本日はおつかれさまでした。 いやぁ、楽しかったですね。ぼくは第一不完全性定理の別証明あたりから、わけがわからなくなってしまいましたが、それでも直接田中先生のお話を聞けてよかったです。 それと、もっと積極的に声をかけていれば、みなさんとお会いできたと思うのですが、すいません、ちょっと緊張のため固まってしまいました笑（実はかがみさんの前に座っていらっしゃった方に最初、声をかけてはみたんですけどね。（「あのーすみません、かがみさんですか？」「いえ、みなみです」と。非常に無礼なことをしてしまいました。）） また機会があればよろしくおねがいします。";
d[1] = "2009-10-31 23:11:18";
n[2] = "かがみ";
m[2] = "今日は本当に楽しい時間を過ごさせて頂きありがとうございます。ゴールドバッハについてはもし ZF でその否定が証明可能であれば「標準モデル」でその否定がなりたつと思います。したがって標準モデルでゴールドバッハ予想が成立すれば ZF で反例が成り立つ可能性はないと思います。もしかして ZF 上のあるモデルで反例が成り立つ可能性があるというならば (Σ_1 健全性についての関連よく分からないのですが) その通りだと思います。間違っていたらごめんなさい。";
d[2] = "2009-11-01 03:14:45";
n[3] = "かがみ";
m[3] = "いや。本当に申しわけございませんでした。みなみさんは髪の毛たくさんあったじゃあないですか。目の前に明らかに髪の毛の不自由なおじさんがいたのに残念でした。何かの機会に一度お会いしたいです。多分お会いできる機会がまたあると思います。そのときはよろしくお願いいたします。";
d[3] = "2009-11-01 03:17:09";
n[4] = "tri_iro";
m[4] = "こちらこそ、かがみさんと久しぶりにお話が出来て楽しかったです。 東工大での写真、先ほどメールで送りましたので、ご確認ください。";
d[4] = "2009-11-01 17:03:41";
n[5] = "かがみ";
m[5] = "写真頂きました。ありがとうございます。色々お世話になりました。出来ればまたお会いできる機会があればうれしいなと思っています。";
d[5] = "2009-11-01 20:37:36";
n[6] = "てなさく";
m[6] = "＞ PA |- (Bew([A]) -&gt; A) のとき PA |- A これは第二不完全性定理から導かれるんですね. A に ⊥ を代入したものは第二不完全性定理そのものですもんね. 成立するから証明して来いと言われれば証明できますが, もちろん知らなかったし, 思いつかないですよこんな定理.";
d[6] = "2009-11-02 14:51:16";
n[7] = "てなさく";
m[7] = "証明できたと書きましたがよく見たら間違ってました... ションボリ...";
d[7] = "2009-11-02 15:18:13";
n[8] = "標準モデル";
m[8] = "健全性の話は不完全性関係の専門書じゃないと載ってませんが、Loebの定理は最近の教科書だと寧ろ証明付きで載ってる方が普通かなーと。Endertonには載ってるはずです。東大出版会のシリーズの緑の巻にも。 第二不完全性定理とは互いに片方からもう一方を導出できますが、この定理が出てきたときに「ああ、当たり前のことだ」と思える人は少ないんじゃないでしょうか。不完全性定理がいくら独学しやすいとは言っても、この定理だとかPeano算術上のreflectionだとかになると結構難しいものがあるんじゃないかと思います。 ちなみにCurryの逆理はLoebの定理の証明の議論と似ているということで、Loebの定理と呼ばれることも多いらしいです。個人的にはあまり良く関連を分かってないんですが。";
d[8] = "2009-11-02 23:43:25";
n[9] = "かがみ";
m[9] = "てなさくさんがご存知なかったとはちょっと意外でした。「ゲーデルと20世紀の論理学3」の98ページに証明が載っていたので読みました。読んで論理は追いかけましたがよく分かっていません。田中先生の資料では数行で「説明」されていましたが、「PA+論理式」が無矛盾なので (PA+論理式) |- Con(PA + 論理式) が成り立ち矛盾という感じの「説明」で、もちろん一般向の人にアイディアを伝えたいということは分かるのですが、どうなのかなと思った部分ではあります。その辺を注意してお話を聞けば大変面白かったです。でも一般に数学の専門家の方からは素人数学愛好者は厳密な証明を理解できないと考えられているのかも知れません。気にしすぎかなと思いますがその点についてはちょっと不本意です。 健全性については全く興味がなかったのですが、今回の講演を聴いて興味がわいてきました。真面目に勉強する時間も能力もありませんが、今までのように拒絶してしまうのではなく、言葉に接したとき真面目に考えたいと思います。不勉強にて Curry の逆リは知りません。貴重なコメントありがとうございます。";
d[9] = "2009-11-03 03:12:05";
n[10] = "ふちの";
m[10] = "ええと，これではだめなんでしょうか: PA|- Bew(A) -&gt; A なら，PA,&not;A |- &not;Bew(A) ところが，&not;Bew(A) は PA+&not;A の consistency を表明しているから，不完全性定理により，PA,&not;A |- したがって PA|- A.";
d[10] = "2009-11-03 03:42:40";
n[11] = "かがみ";
m[11] = "あ。たしかにそのような気がします。すると一つ前の私のコメントは誤読でした。失礼いたしました。でも「無矛盾」という言葉が本当に無矛盾なのか Con(T) のことなのか分かりにくい文面だったとは思います。でもこれを誤読するのは明らかに私の力不足です。「ゲーデルと20世紀の論理学3」の定理4.5は必須として定理4.7の証明がやや面倒な理由はよく分かりません。";
d[11] = "2009-11-03 04:04:38";
n[12] = "ふちの";
m[12] = "ついでに言うと，「標準モデルで成り立つこと」というのはいかにも田中さんらしいですね．";
d[12] = "2009-11-03 04:06:36";
n[13] = "ふちの";
m[13] = "今回このコメント欄では誰も問題にしていませんでしたが， PA |- (Bew([A]) -&gt; A) のとき PA |- A というのは，実は，「(Bew([A]) -&gt; A) の PA からの証明が与えたれたときにそれを A の PA からの証明に書き換えるアルゴリズムが（具体的に）存在する」 ということなんですよね．";
d[13] = "2009-11-03 04:17:48";
n[14] = "かがみ";
m[14] = "実はその言葉 (もしかして「真」とは「標準モデルで成り立つ」ということですか？) は私が言い出して、田中先生が「そういうことですがますます難しくなるので」という感じでした。でも「ゲーデルと20世紀の論理学3」の62ページにそのような記述があるので田中先生のお考えはそうなのかなと思います。";
d[14] = "2009-11-03 04:20:47";
n[15] = "てなさく";
m[15] = "かがみさん＞てなさくさんがご存知なかったとはちょっと意外でした。 Endertonの本も「ゲーデルと20世紀の論理学1～4」も持っていますが、なにしろわたくしの目はフシアナですから。 ふちのさん＞すると一つ前の私のコメントは誤読でした。 ふちのさんの「誤読」とわたくしの「ションボリ」はきっと同じようなマチガイだと思います。たぶん。";
d[15] = "2009-11-03 07:24:10";
n[16] = "てなさく";
m[16] = "うわっまたやってしまった。「誤読でした」はかがみさんの発言でした。てなさくが誤読してしまいました。";
d[16] = "2009-11-03 07:30:08";
n[17] = "てなさく";
m[17] = "ああっとつまり何が言いたいかというと、￢Bew[A] は PA+￢A のconsistency を表現しているけれども、ここでの Bew は PA の算術化に関するものであり、これと PA+￢A の算術化に関する ￢Bew[⊥] が同じかどうかというところが引っかかるわけです。つまり、Bew が二つの意味で使われている。";
d[17] = "2009-11-03 07:33:26";
n[18] = "てなさく";
m[18] = "いずれにせよ粗忽なコメントを乱発してかがみさんとふちのさんにご迷惑をおかけしました。もうしわけありません。";
d[18] = "2009-11-03 07:34:17";
n[19] = "かがみ";
m[19] = "色々教えて頂き感謝しております。ですが頭が混乱してきたのでしばらくこの話題にかんする返信は難しいかも知れません。申しわけございません。";
d[19] = "2009-11-03 11:07:19";
n[20] = "通りすがり";
m[20] = "ふちの氏のいわれる証明は、ブーロス＆ジェフリーの本 &quot;Computability and Logic&quot;で、ソール・クリプキが 指摘したといわれるものと同じようです。 ちなみに、ブーロス・ジェフリーの本では、 ヒルベルト・ベルナイス・レーブの可導性条件と、 B &lt;-&gt; (Bew([B]) -&gt; A)なるレーブ文の 対角化補題による構成から、証明しています。 ちなみに　 B &lt;-&gt; (B -&gt; A)　 はカリーのパラドックスのカリー文です。 もともと、レオン・ヘンキンがヘンキン文 Bew([A]) &lt;-&gt; A を考え、これが証明可能かどうかという 問題を出したのが始まりだとか。 スマリヤンはこのネタが好きらしくて 彼の本ではしつこく扱ってます。 ちなみに第二不完全性定理にしてもレーブの定理にしても 可導性条件が必要になるので、これが成り立たないと 実は証明できない、というのはよくいわれるところです。";
d[20] = "2009-11-05 22:07:07";
n[21] = "通りすがり";
m[21] = "＞「(Bew([A]) -&gt; A) の PA からの証明が与えたれたときに ＞　それを A の PA からの証明に書き換えるアルゴリズムが ＞　（具体的に）存在する」 これは私の憶測ですが・・・ (Bew([A]) -&gt; A)が証明できるとすると その証明はAの証明と同じなんでしょう、きっと。";
d[21] = "2009-11-05 22:28:35";
n[22] = "かがみ";
m[22] = "通りすがりさん、コメントありがとうございます。何か一言書きたいところですが完全に私の能力を超えています。すみません。今後ともよろしくお願いいたします。";
d[22] = "2009-11-05 23:42:22";
n[23] = "通りすがり";
m[23] = "↓でいいように思うのだが。 PA |- (￢CONS -&gt; Bew(A)) なので PA |- (￢Bew(A) -&gt; CONS)　…(*) つまり PA,￢A |- ￢Bew(A) なら(*)より、 PA,￢A |- CONS なので、不完全性定理より PA,￢A |- ";
d[23] = "2009-11-06 08:49:20";
n[24] = "通りすがり";
m[24] = "↑は最後の&quot;不完全性定理より…&quot;が誤りだった。 全然ダメじゃん！ インフルエンザ？で大変なところ、どうもすみません(--ゞ)";
d[24] = "2009-11-06 09:15:06";
n[25] = "かがみ";
m[25] = "通りすがりさん、こんにちは。もう本当についてゆけません。気の利いたコメント書けなくてごめんなさい。";
d[25] = "2009-11-07 00:33:55";
n[26] = "通りすがり";
m[26] = "第二不完全性定理に関しては、あくまでBewの定式化次第だ、ともいわれてます。 Rosserのやり方だと、無矛盾性は証明できてしまうので。 このあたり、根っこをたどると、そもそも「証明が存在する」という性質を算術化しようとした場合に、帰納的述語で表現できない点に行き着くと思われます。 (帰納的でない場合には、完全性定理により、ノンスタンダードな解釈を許すことになる。) その意味では、無矛盾性証明の計画は、第二不完全性定理以前に、「証明が存在する」という性質が、スタンダードな解釈のみを許す形で表現できない時点で、壁にぶち当たったと考えたほうがよいかと思います。";
d[26] = "2009-11-14 16:02:13";
n[27] = "かがみ";
m[27] = "すみません。こちらの方は頭が飽和してついてけない状態です。Bew の解釈はなんというか不思議な感じがします。ローサーの方も理屈としては分かるのですがなんか都合が良過ぎるような。ロジックや集合論には「都合が良過ぎる」定理がたくさんあるのは知っています。なんかとりとめがなくてすみません。こちらの方面は本当に苦手です。";
d[27] = "2009-11-14 21:12:05";
n[28] = "catbird";
m[28] = "2より大きな偶数は、2個の素数の和で必ず表せると、ゴールドバッハは予測しました。例えば14は、3+11＝7+7と2つの素数の足し算で表現することが出来ます。実際にコンピュータで5×10の17乗の偶数まで成り立つことが証明されています。この事実は、何を意味しているのでしょうか。 偶数は、等しい2つの数に分けることが出来ます。偶数（2Ｐとする）を2つに等分した（Ｐとする）一方から、ある数（Ａ）を引き（引いた後をＸとする）、他方にその数（Ａ）を足し（足した後をＹとする）、ＸとＹが共に素数である様なＡが必ず存在すれば、予測は証明されます。 Ｙ＝Ｘ+2Ａと表されます。表を使ってイメージを伝えます。横線の左端を0、右端を2Ｐとし、中間点をＰとします。元々、ＸとＹはＰ上にあります。Ｐが素数であれば、ＸとＹを動かさなくても済みます。偶数（2Ｐ）＝Ｐ（素数）+Ｐ（素数）と表されます。そうでない場合は、ＸをＡだけ0に近づけなければならず、その分ＹはＡだけ2Ｐに近づきます。 0からＰまでの間には、素数が2から順番に3・5・7・11・13・17・19・23・29（どこまでも続きますが、説明の便宜上10個までとします）と順番に並んでいます。Ｐから2Ｐまでには、0からＰ間にある10個の素数の倍数が並んでいます。そうして、0からＰ間にある素数の位置にＸを置いた場合、Ｙが0からＰ間にある10個の素数の倍数位置に来なければ、Ｙは素数となります。（素数の倍数の位置にＹが来ると、Ｙは素数ではなくなります） Ｐが、0からＰ間にある10個の素数である、2から29までのいずれかの素数で割切れる場合は、その位置にＸを動かしても無駄です。Ｙがその素数の倍数になるからです。（ＰはＸの倍数となる。Ｐ＝Ｘ+Ａなので、ＡもＸの倍数である。従ってＹ＝Ｘ+2ＡもＸの倍数となり、Ｙは素数ではありません）その場合と、Ａ＝Ｘ/2の場合以外は、ＹはＸを置いた位置の素数（Ｒとする）の倍数にはなりません。 そうして、Ｘを0からＰ間にある全ての素数上に置いたとき、Ｙが全ての場合において、0からＰ間にある素数の倍数の位置に来た時のみ、Ｙは素数ではあり得なくなります。その時のみ、偶数（2Ｐ）を2つの素数（Ｘ・Ｙ）で表現することは出来ないと言えます。 　偶数（2Ｐ）を2つの素数で表現出来ない確率は、偶数（2Ｐ）が小さい間は、大変低いと言えます。Ｘを置くことが出来る位置は、素数の位置のみです。素数10個の例で説明すると、Ｘを10箇所の位置に置いて見て、その10回全てにおいて、Ｙはその10個の素数の倍数位置いずれかに来なければなりません。1回でもそれらの倍数の位置に来なければ、ＸとＹは素数となります。Ｘを置くことが出来る位置は10であるのに対して、Ｙが来られる位置は非常に沢山あります。しかも、10回中1回でも来る事が出来れば良いのです。 　従って、偶数（2Ｐ）が小さい内は、2つの素数で表せない確率は大変低いと言えます。しかし、偶数（2Ｐ）が大きくなるに従って、0からＰまでに現れる素数が多くなって行き、Ｐから2Ｐ間においては、増えた素数の倍数がどんどん除かれて行き、素数は次第にまばらに成って行きます。そして、偶数（2Ｐ）が大きくなるに従って、ＸとＹが共に素数となれる確率は、低下して行きます。偶数（2Ｐ）が極端に大きくなると、Ｐから2Ｐ間に素数が全く存在しなくなることもあり得ます。その場合、偶数（2Ｐ）は決して2つの素数では表せません。 コンピュータで確認出来た範囲は、まだ偶数が小さく2つの素数で表現出来る確率が高かった為そうなっただけです。ゴールドバッハの予測は、言い換えれば、偶数が2つの素数で表せる確率が高い時には、その偶数はその2つの素数で表せると、当たり前の事を言っているだけだったのです。 ";
d[28] = "2011-02-13 02:35:46";

(password)