数学基礎論・数理論理学　その10

1 名前：１３２人目の素数さん [2011/10/29(土) 22:42:36.86 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その9 kamome.2ch.net/test/read.cgi/math/1317639944/ 166 名前：153 [2011/11/03(木) 17:14:05.37 ] RCA0とWKL0の違いはチューリングマシンの違いですね。 確かに次数やクラスは1つの視点ですね。 167 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:22:16.38 ] >>166 具体的に説明されたい。 168 名前：8 [2011/11/03(木) 19:15:30.11 ] >>152 複雑だけど¬と→だけできる。 ¬(A→¬B) ¬(A→B) ¬(¬A→¬B) ¬(¬A→B) の4つで1パターンで真になる命題が網羅できるので、 これの否定で3パターン真で命題が網羅できて、 4つの内2つを組み合わせて2パターンで真になる命題を網羅する。 4つ全部を組み合わせて恒真、その否定で偽をつくる。 これで16パターンが網羅できる。 169 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 19:49:36.91 ] >>148 証明可能性を描画可能性になぞらえているのか？ コッホ曲線をどうやって描画する？ 170 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 20:22:00.87 ] >>163 まぁ、簡単にいうと、ガロア理論の 本質とは、 ある集合の構造を調べるときに、その集合を直接調べるのではなく、 その集合からその集合への写像の族を考え、 その族の構造を調べることが有効である。 ということ。それ以降の数学のあらゆる所で出てくる重要な考え。 171 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:16:48.67 ] >>170 わざわざガロア理論とか数の演算の本質とかいうから 実に高尚極まりない整数論の奥義を語るかと思えば 数学のどこでもでてくるヌルい一般論じゃんｗ 172 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:22:30.85 ] >>171 >>151が、ガロア理論を誤解して過小評価していたので、 ガロア理論の本質論が出たまで。 そう、今ではいたるところに普及した 重要な考え。 173 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:36:59.04 ] >>172 ガロア理論の本質でもなんでもない。 例えば、ガロア理論→幾何学、集合→空間、写像→変換と置き換え 「幾何学の本質とは 　空間の構造を調べるのに、空間を直接調べるのではなく 　空間から空間への変換の族を考え、 　その族の構造を調べることが有効だということ」 といっても通じてしまう。 こんなヌルイ一般論を重要というのは・・・馬鹿ｗ 174 名前：１３２人目の素数さん [2011/11/03(木) 21:37:49.72 ] >>168 その4つの式の最初に¬をつける意味は？ 175 名前：１３２人目の素数さん [2011/11/03(木) 21:46:35.36 ] >>174 ¬(A→¬B)＝A&B ¬(A→B)＝A＆¬B ¬(¬A→¬B)＝¬A&B ¬(¬A→B)＝¬A&¬B と思われ。 176 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:50:53.37 ] 以前ツイッターで 「複素数は本来、数じゃ無い！」 とわめいていた数学者(？)がいた。 実数ではなく複素数、というところが素人っぽくて面白い。 どうも、全順序集合でないと、本来の数ではないらしいｗ 177 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:55:30.41 ] 角度の値は、実数ではなく円周群の要素と考えたほうがいい。 円周群の要素を数と呼ばないのは、どう言い訳しても手抜かりである。 178 名前：8 mailto:sage [2011/11/03(木) 22:03:22.17 ] >>174ない。 179 名前：１３２人目の素数さん [2011/11/03(木) 22:04:44.77 ] 辞書的順序入れれば複素数も全順序になるよ 180 名前：８ [2011/11/03(木) 23:21:16.14 ] ¬と∧∨は1つの述語にまとめられる。 A○Bを¬(A∧B)、 A◎Bを¬(A∨B)で定義すれば どちらも2項述語1つだけで真理値表をすべて満たす。 A○Bの否定が(A○B)○(A○B)になったりする。 代数の演算を考えれば自明だが。 181 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 23:21:35.62 ] >173 ガロア理論の重要なところの一つはその一般化できる構造なんじゃないの？ ガロア理論の説明で良く幾何学の証明不可能性の話が出てくるから そうなんだと思ってたけど。 182 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 04:35:29.49 ] >>160 ほんじゃガロア理論のごく一部であるところの 代数解の不存在云々（アーベルの定理？）は 二次的なので重要でないってことでおk? つーか、ガロア理論の一部とか思ってるの？ 一部ではなくて、単に金字塔的な応用例ってだけだろｗ 君こそ勉強しなおしてきたらどうだい？ 183 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 05:04:11.68 ] >>176 実数ってのがそもそも「数」ではない。実数で表されるものは「量」だ。 従って「数学」という名称は名が体を表していない。「量学」と改称すべきである。 184 名前：１３２人目の素数さん [2011/11/04(金) 06:36:50.32 ] >>183 量と数と実数の関係をはっきり述べないと議論にならない 185 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 07:13:03.86 ] >>184 こんな定義だそうだ： kamome.2ch.net/test/read.cgi/math/1317089920/21 186 名前：１３２人目の素数さん [2011/11/04(金) 08:02:31.27 ] >>185 要するに 離散量＝自然数＝真の数 連続量＝実数＝数でない といいたいわけか。 なんか窮屈だな。 窮屈を好むのはやっぱ精神異常？ 187 名前：１３２人目の素数さん [2011/11/04(金) 08:04:26.33 ] なんでもかんでも数と呼んだらええんちゃうｗ 自然数も有理数も実数も複素数も四元数も数。 それどころかベクトル空間の元も数。だから関数も数。 ええい、もう、集合も数とよんだらええがなｗ 188 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:13:49.78 ] 人数とか個数とはいうけど、水数とは言わないだろ、水量だ。 つまり日本語の「数」は、本来連続量には使われない。 連続量である実数に「数」とつけるのはテクニカルタームでだけだ。 189 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:14:59.70 ] いま思ったが、数学で扱うものはみな集合だから 数学は集合論だってことだなｗ。 ということで、数学板を集合論板に改名すべしｗ 190 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:18:33.42 ] >>188 もうええよ、数学も量学もせますぎ。 今の数学は全て集合論だからｗ ♪これも集合、あれも集合 　たぶん集合、きっと集合 191 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:23:09.84 ] >>190 というと、圏論ヲタから 「圏の重要性を全く無視している！」 といわれそうだな。 それなら、まあ、圏論の立場も立てて 数学板を集合論・圏論板に変えるのはどうだ？ｗ 192 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 09:27:38.04 ] >>181 ガロア理論の胆は、 集合(体)の構造を調べたい時に、 その集合上の写像の族(変換群)の 族としての構造(群構造)を調べるという所。 個々の写像が具体的にどの元をどの元に 移すかどうかは忘れて、写像の族が織り成す 性質(群としての性質)を調べるという所。 ここに既に圏論の考えがある。 193 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 09:59:33.66 ] 上がガロア理論の本質だけど、 代数方程式に絡めて、もう少し詳しく書く。 有理数係数代数方程式に代数解があるということは、 有理数体に解を付加した体が、 有理数体に1の冪根を付加した体の 部分体になっていること。(本当は嘘だが遠くない) だから、ある体はある体を部分体をもつか？ という問題になる。 体上の(自然な)変換群を考えると、 部分体と部分変換群との間に自然な対応がつく。 (ここがガロア理論の胆。以下は代数的な話) 有理数体に冪根を添加したという特別な体に対し、その体の変換群は、冪根の性質からある制約をうける。その制約は、部分変換群へも伝播し、対応する部分体へも伝播する。 この部分体が、有理数体に代数方程式の解を添加した体なら、その制約は、 その代数方程式へも伝播する。 五次以上の代数方程式では、この制約を外れるものが出る。 こういうシナリオです。 194 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 20:05:57.67 ] 逆数学が二次的って言われるのは、 ある定理や理論にどの公理がどの程度本質的に効いてくるのか ってことが分かるってのがメインで、基本的にはそれ自体から 数学のレベルで新しい定理が出てくるってわけじゃない （メタレベルで数学がより分かるようになるだけ）って意味じゃねーの？ 195 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:07:21.61 ] でも、再帰的に逆数学の定理も素材になるじゃん。 196 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:48:52.44 ] >>195 逆数学が逆数学自体を研究対象にしたところで、それが数学からみて 二次的な存在であることは変わらない（というかむしろ三次的存在になってしまう） のではないの？ 197 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:53:55.21 ] >>194 そういうことを言いたいのであれば、最初からそう言えばいい。 例のアホは、そんな詳しいことは言ってない。 「逆数学は二次的だ」としか言ってない。だから A：じゃあガロア理論も二次的だな。 B：何を言うか。お前はガロア理論を分かってない。 とかいうワケの分からない方向に進むのだ。Aが言っていることは 「お前の言う いい加減な "二次的" に従えば、ガロア理論だって 　二次的になってしまうぞ。それでいいのか？」 ということである。すなわち、Aの発言の本質は 「 "二次的" とは何なのか詳しく説明しろ 」 ということであり、Aが問題にしているのは "二次的" の定義である。 従って、A自身はガロア理論のことを "二次的" だとは思ってない。 Aは、"二次的" という内容を皮肉っているだけである。 実際、>>151の書き方は明らかにこのような意図に読める。 よって、Bのような返答は見当違いであり、正しい返答の仕方は 「 いや、二次的とはこういう意味だ。ガロア理論はこの意味で二次的では無い 」 というものでなければならない。"二次的" の定義に触れない返答は意味が無く、 話がこじれるだけである。 198 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:57:25.73 ] 要するに>>197は話にならんレベルのアホってことか。了解した。 199 名前：１３２人目の素数さん [2011/11/04(金) 21:59:57.78 ] 答えられないから逃げるね まで読んだ 200 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:02:01.64 ] >>198 いくら煽っても、例のアホが何も言ってないことには変わらない。 今の段階で分かっていることは ・例のアホ本人による、「逆数学は二次的だ」の説明が未だに無い。何も言ってないのと同じ。 ・別人である>>194による、「二次的だ」の見解は登場している。 ということにすぎない。 201 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:06:55.85 ] まあいくら誤魔化したところで、そんなつまらないことをいつまでも愚痴愚痴ネチョネチョやってるアホが 一人居るってことはずっと変わらんということにすぎない。 202 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:24:51.74 ] まあ、いくら つぶやいたところで、例のアホが何も言ってないことには変わらない。 圏論スレのころから内容が全く無い。 203 名前：１３２人目の素数さん [2011/11/04(金) 22:29:58.48 ] ガロア理論に先行する圏論の萌芽はないの？ 204 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:47:08.09 ] >>197 他人に日常用語の定義定義とうるさくて、 当の本人は何も定義しないし、何も主張しない。 他人の話にケチつけてれば自分の立場が 崩れないと考えている。完全なアホ。 自分がアホ出ないことを主張してみな。 205 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:52:44.88 ] アホ本人を納得させるつもりで書いてないから。 第三者(特に若者)がみてこっちに分がありそうだと 思ってくれればそれでじゅうぶん。 206 名前：１３２人目の素数さん [2011/11/04(金) 23:08:22.36 ] >>205 君には分がないよ。 よく考えればわかるので説明はしない。 207 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 23:29:45.39 ] あ、言っとくが、二次的という言葉で 逆数学を最初に批判したのは私じゃない。 でも充分私には言いたいことは伝わった。 私は彼に分があると思った 208 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 01:19:12.75 ] >>194 代数的解法があるかどうかはメタレベルではなく数学の問題だと？ ある定理や理論にどの公理がどの程度本質的に効いてくるのかは二次的で ある解を求めるのにどういう手法（代数的か超越的か）が本質的に必要かは一次的なのか？ 随分と恣意的な境界線だこと。というか逆数学を二次的にするための定義だな。 「二次的とは逆数学のようであること」と言っているのと大差ない。 209 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 02:09:51.06 ] 二次的だと狭いってのも意味不明だな 210 名前：１３２人目の素数さん [2011/11/05(土) 02:16:07.40 ] ﾁｮｲｽしてはいけない公理をﾁｮｲｽするから球分割の矛盾が生じるのだ 211 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:16:55.47 ] ちゅうか、「方程式を代数的に解く」ってのは数学の話で、 連続体仮説を公理に入れるか入れないかはメタ数学の話で、 重力を含む超統一理論があるかどうかってのは物理学の話で、 ……etc. って中で、数学のレベルでの話以外は数学にとっては二次的三次的なもんだろ。 どんだけ頭沸いてるんだか。 212 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:23:28.11 ] で、その「数学のレベル」ってのはなんなんですかね。 213 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:35:16.66 ] >>211 それって「逆数学は重要でないから重要でない」とか言っているのと同じだから。 真面目に議論する気がないなら出て行ってね。 214 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:38:54.08 ] >>213 逆数学は逆数学で、 逆数学からすれば数学も物理も国文学も等しく二次的三次的だ と言っているのに、君こそまじめに話する気がはじめからないんだろ？ 215 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:41:12.51 ] つか、>>214は二次的＝重要でないとか、言ってるも同然なんだが、 んなわけないだろ、ドンだけ頭悪いんだこの阿呆は 216 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:42:03.55 ] おっと、滑った。 つか、>>213は二次的＝重要でないとか、言ってるも同然なんだが、 んなわけないだろ、ドンだけ頭悪いんだこの阿呆は 217 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:13:40.16 ] dictionary.goo.ne.jp/leaf/jn2/166890/m0u/%E4%BA%8C%E6%AC%A1%E7%9A%84/ にじ‐てき【二次的】 ［形動］主となる物事に対して、それに付随する関係にあるさま。また、ある物事から派生したもので、それほど重要でないさま。副次的。「―な災害」「―な問題」 218 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:18:53.04 ] １．主となる物事に対して、それに付随する関係にあるさま。 ２．また、ある物事から派生したもので、それほど重要でないさま。 ３、副次的。 ってのは意味が並立なわけだが。 219 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:19:44.54 ] 辞書も読めないとか、やっぱり幼稚園児並の脳みその持ち主だったｗ 220 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:21:54.87 ] 逆数学は二次的　と最初に言ったのは>>135 二次的＝狭い　と最初に言ったのも>>135 二次的＝重要度が減る　と最初に言ったのは>>139 >>135にとっては、逆数学は二次的で、狭い >>139にとっては、逆数学は二次的で、重要度が減る 二次的だとなぜ重要度が減るのか、あるいは、 二次的だとなぜ重要でないのか、そのことに答えたレスはまだない 二次的だとなぜ狭いのか、そのことに答えたレスもまだない とりあえず、スレを見渡す限りは、二次的だと重要でないという考え方は マイナーのようである 221 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 04:24:29.24 ] 並列なら「二次的＝重要でない」も正しい解釈の一つ。 従ってそれを「んなわけないだろ」と言っている奴こそ辞書が読めないんだな 222 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:26:00.30 ] いや、>>217で答えは出ていたか そうか、最初から重要でない意味が含まれているのか 223 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 04:27:53.94 ] ワロタ藁ｗ 224 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:05:00.64 ] >>221 並立なんだから、他の意味で言っている場合を完全無視して 「二次的＝重要でない」と言ってると主張するのは、 幼稚園児にも笑われるレベルの阿呆だ。 225 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:09:13.82 ] 正しい解釈の一つである可能性を無視して 「んなわけないだろ」だろと全面否定した人間は 幼稚園児に笑われるレベルだろ 226 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:14:54.56 ] 並列に複数の意味がある言葉は、文脈によって最も適切な意味で解釈するべきであろう。 しかるに139が「二次的であれば重要度が減る。」と述べている。 更に逆数学批判派は同語反復的な主張が多数であった。 かような文脈において、二次的＝重要でない、という解釈は 139の発言をまさに同語反復とするものであり、 この文脈において最も適切な「二次的」の解釈であると考えられるのである。 227 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:17:26.03 ] というか、俺も逆数学は数学にとって二次的だというレスをしているが、 全く逆数学批判派ではないぞ。そこまで興味を持っても居ないが。 228 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:18:16.08 ] 重要度が減ると重要でないをイコールで結ぶのはさすがに赤ん坊以下だよ。 229 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:32:12.01 ] 逆数学が副次的なものでないという主張の意味が分からん。 230 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:47:21.72 ] >>228 お、辞書の読み方では勝ち目がないと悟って論点のすり替え？ しかし残念だが>>226の主張は「重要度が減る」と「重要でない」の同値は必要ない。 後者から前者への implication さえあればいい。 231 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 08:01:47.04 ] 俺は逆数学は、二次的だとは思わんな。寧ろ根本的だろう。 例えばRCA0とWKL0の違いが明らかになったのは面白い。 前者は明らかに構成的だが、後者は何らかの超越的な仮定がある。 こういうことに対して何の面白みも感じない人は 数学的感覚が鈍磨しているといっていい。 232 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 09:09:38.10 ] >>231 それって単なる盆栽趣味。ないしはスケールが小さい。 ないしはスケールの大きな数学を知らない 233 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 10:21:18.06 ] >>232　スケールの大きいことをやりたがる人は 数学なんかやらないｗ 微細構造を好む人がやるのが数学。 234 名前：１３２人目の素数さん [2011/11/05(土) 10:28:58.83 ] 計算理論の壮大さを知らんようだな。 全数学を包括しかき回すほどの規模。 21世紀の主流は計算論＋理論計算機＋集合論 235 名前：１３２人目の素数さん [2011/11/05(土) 10:35:20.73 ] >>234 別に壮大だとは思わない。 そもそも壮大だからスゲーとはおもわんし。 なにかといえば大きさを求める奴は きっと●ん●んが小さいんだろうｗ いっとくけど、♀の＊＊＊は鈍感だから 入れたって正確な大きさなんかわかりゃ せんってｗ 236 名前：１３２人目の素数さん [2011/11/05(土) 12:13:54.61 ] 逆数学が2次的ってｗ 本来逆数学のような計算論の視点が1次的で、 これまでの数学が2次的なものなのだが。 ユークリド言論が1次的で非ユークリッドが2次とか言っているようなものw 237 名前：１３２人目の素数さん [2011/11/05(土) 12:18:44.87 ] >> 234 これ興味あるからもうすこし聞かせて。 オレは、本当にそうであればよいと思う者だが、今の計算論や理論計算機にそんな兆候があるか？ 何あるいは何処がその兆候だと思うんだ？ 238 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 12:23:15.54 ] >232 無限と同じぐらいの深淵じゃないの？ 可算数と非可算数の境界の話だよね？ 239 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 13:58:14.73 ] >>236 逆数学にとって数学が二次的な対象でしかないことは誰も否定して無いと思うが。 240 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 14:49:37.41 ] >>239 逆数学は、直接、数学の成果を得る活動ではないが その結果が、数学でないかといえば、そんなことはないから 結局、フツウの数学と変わるところはない。 241 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 17:17:43.15 ] 逆数学の井の中の「数学」を大海の数学と称する腹か。 自分で「フツウの数学」と区別しておいてそれは詭弁ではあるまいか。 242 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 17:25:08.36 ] >>241 要は対象の選び方の違いにすぎない。 こんなことに難癖をつける奴は●違いだろう。 243 名前：１３２人目の素数さん [2011/11/05(土) 19:00:04.00 ] >>243 述語論理ですが、 言語Lってのは 論理的述語記号∧、∨、¬、→、∀、∃ 変数記号x1、x2、x3、... 関数変数記号F1、F2、F3、... 述語変数記号R1、R2、R3、... の記号の組合せの事ですよね。 この記号の組合せの総数、つまり2^Lの中で、 変数記号、引数に項をとる関数の形をしたものが項ですよね。 項の集まりをTermとすればTerm⊆2^Lになりますよね。 引数に項をとる述語と、述語を引数にとる論理的述語が論理式ですよね。 論理式の集まりをFlmとすればFlm⊆2^L。 244 名前：１３２人目の素数さん [2011/11/05(土) 20:50:08.36 ] LによってTermやFlmが規定されることから、 これらをTerm(L)やFlm(L)と書き換えよう。 M(L)という対が＜M,Pri,Fnc,m,v＞と定義される。 Mは集合。 Priは定義域がMを動く述語の集合。 Fncは定義域・値域がMを動く関数の集合。 mは定義域が定数記号ならば値域がM、 定義域が述語定数記号ならば値域がPri、 定義域が関数定数記号ならば値域がFnc、 となる全単射関数。 vはFlm(L)から{0,1}への関数。 さてここまで来れば私の主張したい内容が想像つくだろう。 つまり、「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」 245 名前：１３２人目の素数さん [2011/11/05(土) 21:23:51.57 ] >>244 ＞「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」 上記の文章は理解できない。 もし、 「論理記号によって書かれた述語だけを 　述語として認めるのはおかしいだろう？」 といいたいのであれば、全くその通りである。 実は一階述語論理と二階述語論理の違いはそこにある。 一階述語論理では、論理式として書けるものしか拘束できない。 しかしながら、二階述語論理では、述語全体を束縛する演算子 として∀、∃を用いることができる。 246 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 21:33:28.20 ] >>241 ははは。 基礎論って、妖怪人間ならぬ妖怪数学みたいなものか？ 普通の人間や数学は、日夜、立派な人間や立派な数学になりたいと 切磋琢磨しているのに、 普通の人間か数学になりたい、それで充分だからならせてくれと。 247 名前：１３２人目の素数さん [2011/11/05(土) 22:09:00.71 ] さて、途中まで書いていたのだが以下続き。 論理的述語記号は通常、 A　B　A∧B ------------ 1　1　1 1　0　0 0　1　0 0　0　0 のような真理値が定義されているのだが、 これはいささか早計ではないだろうか。 これが前提となるのは非常に不快である。 そこで論理的述語記号を関数や述語と同様に、 論理的述語変数と論理的述語定数に分離して考えてはどうだろうか。 つまり論理的述語記号∧、∨、¬、→、∀、∃ を 論理的述語変数L1、L2、L3、... にすげ替えてしまうのである。 同時に論理式の定義を以下のように拡張する。 ・引数に項をとる述語。 ・引数に引数に述語か論理的述語をとる論理的述語。 248 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 22:27:27.03 ] >>211 同意。 逆数学や基礎論と数学は別物。 別物なんだから、価値観が違う。 基礎論にとっては、代数方程式論より逆数学のほうが重要かもしれないが、 数学にとっては、代数方程式論の方がはるかに大事。 価値観が違うんだから、はっきり分けるべき。 数学は数学。論理学は論理学。 刃物をつかっているという点では同じでも、 サムライと板前くらい違う。目的も価値観も違う。 249 名前：１３２人目の素数さん [2011/11/05(土) 22:32:31.65 ] >>245 まったくそのとおりである、私はさらにその考えを推し進めようとしている。 注意すべきは論理的述語は引数に直接項をとることができない。 これは既存の1階述語論理と同様である。 （いや、∀と∃の存在保証が失われた今、1階というのは意味をなさない言い方か。） さて、今述語論理の言語は以下の述語を持つ。 論理的述語変数 L0、L1、L2、... 論理的述語定数 - 非論理的述語変数 R1、R2、R3... 非論理的述語定数 - ここで論理式の定義と比較したとき、ある事実に気が付くだろう。 論理式の非論理的述語は引数に項をとる。 論理式の論理的述語は引数に非論理的述語と論理的述語をとる。 つまり項で非論理的述語の真偽が決まり、非論理的述語で論理的述語の真偽が決定する。 250 名前：１３２人目の素数さん [2011/11/05(土) 22:54:57.82 ] 非論理的述語を1階の述語、 論理的述語を2階の述語と考えると、 当然3階4階...n階と階層化をすすめたくなる。 重要なのは、n階の述語は引数にn階以下の述語をとるということ。 そして1階だけが極小の述語となり、引数に項しかとれない。 述語はどの階層でも真偽が決定するが、項は単独では真偽決定できない。 251 名前：１３２人目の素数さん [2011/11/05(土) 23:29:23.60 ] さて、構造の側はどうするかというと、 {Pri_n(L)}n∊N とでもして述語を階層ごとに分けとけばよいだけだ。 さて言語Lの論理式は今や以下の定義となる。 ・項を引数に持つ1階述語。 ・n階以下の述語を引数に持つn階述語。ただしn≧2。 こうすると構造の側はどのように真偽を判定するのか。 なおn階の述語すべてのアリティの個数制限をなくす。 252 名前：１３２人目の素数さん [2011/11/05(土) 23:45:50.00 ] なお真偽値をいくつにしても構わないし、 どういった場合においてもここまで一般化された 言語では任意の証明体系で完全性定理が成り立つ。 というより論理記号がないため恒真が意味をなさない。 こう考えると1階述語論理とは、 述語が2階までで、 2階の述語定数記号が各アリティ2の∧、∨、¬、→、∀、∃ である。 ここで通常の1階論理と同じような真理値を2階の述語に与えれば良い。 （勿論構造の側の解釈を与える全単射の関数mもn階分に対応している。） また、高階述語論理や様相論理も自由に展開できることを確かめたれたい。 了 253 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:12:56.62 ] 話をバッサリ切ってごめんけど、なんでこんなに難しい文章で説明しようとするの？ 254 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:14:56.35 ] バカだから 255 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:18:17.96 ] ロボットに説明するわけじゃあるまいし。 何で数学の証明とか解説ってやたら難しい事書くんだろう。人間が人間に説明するんだから(ry 256 名前：１３２人目の素数さん [2011/11/06(日) 03:51:17.42 ] >>255 解釈の方法を限定するためじゃね。 自然言語で意味が一意になるように書くと、更に長くなるよ。 試しに選択公理を論理式と自然言語で書いて見比べてみたら。 257 名前：１３２人目の素数さん [2011/11/06(日) 07:15:28.38 ] 難しいと言うか 普通の教科書の書き方をパロッてるんだろう 258 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 08:11:19.75 ] >>248 何がいいたいのか意味不明。 そもそも代数方程式でも解の存在が大事だという人と 解の性質が大事だという人がいるだろう。 数学の中で分野わけすればいいだけのこと。 整数論至上主義者は、整数論のために 関数解析を「数学ではない」といって 切るつもりか？ 259 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 08:18:45.68 ] >>249-252 ゲーデルのLを知らんのか？ あれはまさに無限階論理といってもいいわけだが。 しかし、全ての階をいっしょくたにできるような 最上階というものは存在しない。 260 名前：１３２人目の素数さん [2011/11/06(日) 08:53:31.44 ] さて、いよいよ本論に入ろう。 前回、真偽の決定可能な論理式は1階以上の述語とした。 一方でn階の述語はそれ以下の階層の述語を引数にとるとした。 ここで項も論理式に加えてしまうのが合理的だと思わないだろうか。 また2階以上の階層の真偽が同様に決定するのも不自然だ。 はじめてに論理式の定義を以下のように書き換える。 ・従来の変数は0階の論理式である。 ・従来の関数は1階の論理式である。 ・従来の述語は2階の論理式である。 ・従来の論理的述語は3階の論理式である。 さらに ・n階の論理式はそれ以下の論理式を引数に持つ。 ここで問題が発生する。f(x)∧y、a＜(b＜c) のようなものが発生する。 これは容易に解決する。 261 名前：１３２人目の素数さん [2011/11/06(日) 09:41:26.91 ] >>259 ある段階で導入する可能性もある。 かつて関数vは論理式と真理値を関連付けていた。 これは解釈という考え方で一般化することが可能である。 例えば、従来のx＜y∧y＜zという論理式を考える。 x＜y∧y＜zの真理値は、x＜yとy＜zの真理値によって決定する。 ここでx＜y∧y＜zの真理値とx＜yとy＜zの真理値は実は違うものだと考える。 そして真理値というよりは、例えば集合{t0,t1}を値が動くと考える。 一方f(x)やg(y)は構造の領域Mを動いている。 3階以上の述語も同様にふるまう。 ここで各階の論理式は解釈により集合へ対応付けられる。 各階の論理式に対応する集合は、M0、M1、M2、...とでも定義しておけばよい。 例えばPAの標準モデルは、 M0＝N、M1＝N、M2＝{0,1}、M3＝{0,1}となるだろう。 ここで先ほどのf(x)∧y、a＜(b＜c)。 f(x)∧yだが、f(x)はM1、yはM0に対応付けられる。 ∧は{t0,t1}に対応付けられている。 ここで∧を解釈する関数の定義域が{t0,t1}だけならば、 それ以外の不正な値を定義不能としてはじくことが出来る。 つまり、f(x)∧y、a＜(b＜c)などは決定不能になる。 もちろんM0＝M1＝M2＝...と定義することで 意図的に関数値や定義域を混同させることも可能だ。 つまり完全性定理での論理式が、決定可能な論理式に制限されるだけだ。 262 名前：１３２人目の素数さん [2011/11/06(日) 09:55:54.14 ] ところで真理が真偽2択から解放された今、 モデルの定義も変えねばなるまい。 矛盾許容論理などを考えればモデルとは、 ある言語のすべての論理式を定義可能な領域を持つ構造。 これにより先ほどの完全性定理は再び従来通りの論理式に対するものとなる。 263 名前：１３２人目の素数さん [2011/11/06(日) 10:06:41.41 ] >>260、261 お前アホか。全部既知のことを今頃お勉強が終わったということ。 それからn階なんて言っている時点で古過ぎ。循環だってあるんだから。 264 名前：１３２人目の素数さん [2011/11/06(日) 10:34:01.28 ] >>263 ご立腹かね？ワトソンくん！ 265 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 16:26:20.00 ] 流れをぶった切って。 物理なんかの測定から理論を抽出するところに逆数学的なものを感じるんだけど、 逆数学にそういった応用例とかないのかしらん？ 266 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 16:43:51.03 ] >>243-244　>>247　>>249-252　>>260-261 トンデモ？ 267 名前：１３２人目の素数さん [2011/11/06(日) 17:16:49.63 ] >>266 すでに知られていることを独自の発想のように書いてるスレ潰し 268 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:19:39.30 ] >>267 既知？全く荒唐無稽の既知外だろｗ 269 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:32:12.02 ] >>258 わかってないなぁ。 数学はひとつなの。 関数解析にとっても代数方程式は重要なの。 整数論と関数解析は分けることができないの。 向かう方向はおなじだから。 だが、逆数学はわけることができる。 価値観が違うんだから、どうどうと違う学問だと なのって、数学の外で一国をつくればよい。 関数解析と整数論が違う学問だと思うのは、 きっと、現在の教育を途中で投げ出すと、 そういう感覚を覚えるようになってしまっているのが 原因。 270 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:43:37.04 ] ロジックだって、完全性定理のレベルでさえ、 束、位相、代数が基盤だろ。 271 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:48:05.83 ] >>270 いや、高校数学で充分足りる 272 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:02:19.72 ] ロジックって、一体何を目的にして何に向かって 研究してるの？ 273 名前：１３２人目の素数さん [2011/11/06(日) 18:20:57.12 ] 証明論とかって計算機畑の方が主流？ ここ最近の研究事情がどうなってるのかわからん。 274 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:23:49.45 ] >>269 ＞数学の外で一国をつくればよい。 ずいぶん壮大なことをのたまっているようだが、今の体制で 本当にそのようなことを実現するなら、政治的な力が必要だな。 内部から変化することはありえないから。 こんなところで愚痴ってないで、お前が先頭に立って 排斥運動の1つでもやってみたらどうだねｗ 275 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:28:10.07 ] ロジックというのは、ロジックに関係しているというだけの 雑学の総称？ 276 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:48:03.53 ] 「AはAに関係してるものの総称」 277 名前：１３２人目の素数さん [2011/11/06(日) 19:35:09.95 ] >>276 アニメやゲームはそういう感じで使われているね 278 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 21:24:26.00 ] >>271 基礎的な定理には初等的な証明、理解の仕方があるのは、 代数だって変わらんでしょ。けどそれじゃ数学的構造理解しているとは言えない。 279 名前：１３２人目の素数さん [2011/11/06(日) 21:38:02.64 ] >>243-244　>>247　>>249-252　>>260-261 あなたのスタイルがちょっと古かったりおおげさだったりするのが皆の癇にさわって いるだけかも。既知かも知れんが、学生だとすればなかなか力ある。 しつこくがんばれば将来性あるよ。めげるな。 280 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 22:05:42.78 ] 基礎論による理論の構造分析を、通常数学の学習や理論の創造に役立てたい。 オススメの基礎論学習コースある？ 学習者は代数専攻の数学修士として。 281 名前：１３２人目の素数さん [2011/11/07(月) 05:44:38.12 ] >>279 人を駄目にする褒め方をしてはいけない 282 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 05:50:42.76 ] むしろボロクソにけなしまくる方が駄目にするんじゃねえの？？ 283 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 07:16:52.39 ] >>279 全然見当違い。 そもそも論理式の値が真偽値でないとする発想が既知外。 てゆーか自画自賛だろ。トンデモがよくやる手だｗ 284 名前：１３２人目の素数さん [2011/11/07(月) 07:52:43.55 ] ファジー論理 285 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 08:00:25.69 ] 過去にもいたよね、方程式の解が実数でないものを認めようとしたり 小さい数から大きな数を減じてみようとしたり。 286 名前：１３２人目の素数さん [2011/11/07(月) 10:17:53.15 ] >>285 それを今やって大発見だと思う人がいたら可哀相な人だよね。 287 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 10:28:23.70 ] >>272 とか、 >>280 とか、 真面目な質問に答える能力のある人はいないの？ 288 名前：１３２人目の素数さん [2011/11/07(月) 11:13:58.64 ] じゃあ俺が、 といっても俺も素人なんであんまり真に受けないでね。 さしあたり完全性定理とか不完全性定理を知りたいなら、 朝倉 現代基礎数学 15 数理論理学 鹿島亮著 を読んで、証明とか説明に不足を感じたら J.R.Shoenfied著のMathematical Logic を読めばいいと思う。 モデル理論の代数幾何への応用とかは知らないんで。 289 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 11:50:14.30 ] 完全性定理、不完全性定理は、エンダートンで 勉強しました。その次にくるのは何がよいでしょうか？ 290 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 17:31:06.56 ] >>289 エンダートンを読了したのならば数理論理学に関して一通りの基礎は身に付いたはずなので 次は自分が特に興味のあるテーマのモノグラフやサーベイに進むのが良いでしょう。 291 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 18:52:20.60 ] 代数方面の人なら幾何的モデル理論とかが良いんじゃないかな 別にモデル論の知識は無くても読めるように書いてあるよ 基礎論全般の勉強なら新井敏康の数学基礎論が良いよ 包括的な入門書の中では一番レベルが高いんじゃないかな 292 名前：１３２人目の素数さん [2011/11/07(月) 20:37:37.55 ] Endertonたけぇｗ 仕方ないからこれにしよう・・・ Lectures in Logic and Set Theory: Volume 1, Mathematical Logic (Cambridge Studies in Advanced Mathematics) [ペーパーバック] George Tourlakis (著) 293 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 20:49:01.48 ] >>291 へえ、モデル理論仕込まなくても読めるんですか。 アリ。 294 名前：１３２人目の素数さん [2011/11/07(月) 21:15:27.88 ] モデル理論の代数幾何への応用なら 江田の数理論理学、これは絶対おススメ。 295 名前：１３２人目の素数さん [2011/11/07(月) 22:10:14.58 ] 証明論で良い本ある？ 296 名前：１３２人目の素数さん [2011/11/07(月) 22:48:43.42 ] Umm APPLIED LOGIC SERIESとかCambridge University Pressのコンピュータサイエンスの 論理シリーズは良書が多いねぇ 297 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 23:32:17.19 ] >>294 生協で見たことあるが、そんな特徴ある本なの？ 読んでみないと分からんもんだね。 298 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 17:18:48.13 ] ウィトゲンシュタインの論考ってどうなの？ 基礎論的には。 299 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 18:05:45.72 ] 数学としての基礎論にとっては無価値だろ。 300 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 18:10:42.83 ] 数学として基礎論は無価値だろ。 301 名前：１３２人目の素数さん [2011/11/08(火) 18:54:12.25 ] ウィトゲンシュタインの像とかいう概念を 直観主義で再現するみたいなパワポ見たことあるよ 302 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 20:17:17.36 ] 論理学なんかやって何の意味があるんだ？ 303 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 21:46:59.04 ] もちろん数学の基礎付けですよ！ 304 名前：１３２人目の素数さん [2011/11/08(火) 21:53:03.38 ] 論理学は木の研究 目標は新たな計算機の創造 うひ 305 名前：１３２人目の素数さん mailto:age [2011/11/08(火) 22:39:11.92 ] 論理学なんかで数学の基礎付けができるのか？ 306 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 22:49:07.15 ] 量化の代入的解釈(substitutional quantification )って何ですか？ぐぐってもよくわからなかったのですが。。。 307 名前：１３２人目の素数さん [2011/11/08(火) 23:36:34.25 ] 例えば述語論理で言語の定数が0,1,2のとき、 「∀xP(x)が真」を、「P(0)が真＆P(1)が真＆P(2)が真」 と置き換えて解釈をする流儀。 モデルの側の領域と無関係と考えるような意味論。 ただ強完全性とコンパクト定理が成り立たない。 308 名前：１３２人目の素数さん mailto:sage [2011/11/09(水) 00:09:01.98 ] >>307 なるほど。解説ありがとうございます。 >モデルの側の領域と無関係と考えるような意味論。 領域と無関係というのは、領域自体考えに入れないということですか？ たとえば、普通ならP(0)が真 iff V(0)∈V(P)と考えると思うのですが、上の意味論ではP(0)の真理値はどうやって決まるのでしょうか？ 309 名前：１３２人目の素数さん [2011/11/09(水) 08:14:34.34 ] 例えば P(x)のモデルMでの解釈が{2,3}で、 言語の定数記号がa,b、 そのMでの解釈がそれぞれ2と3だとする。 このとき代入したもの P(a/x)とP(b/x)を解釈すると両方真。 つまり∀xP(x)が真。 ところがモデルMの領域全体がどうなっているかは不明！ 310 名前：１３２人目の素数さん mailto:sage [2011/11/09(水) 13:40:46.76 ] >>309 そういうことでしたか、よく分かりました。 311 名前：１３２人目の素数さん [2011/11/10(木) 15:23:53.16 ] 論理学なんかで数学の基礎付けができるのか？ 312 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 15:25:57.13 ] それは未来人に訊いてください 313 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 16:50:53.13 ] ロジック抜きでどうやって数学を構築するのかと… 314 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 18:28:52.13 ] トポスとか圏論とか 315 名前：１３２人目の素数さん [2011/11/10(木) 18:47:35.69 ] >>314 そりゃ集合論抜きでロジック構築する方法だろ＾＾； 316 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 19:42:13.85 ] 数学の基礎付けがどうとかいうのは 今時（ロジックの中でも）時代遅れで、 研究者はほとんどそんなこと気にしちゃいない 317 名前：１３２人目の素数さん [2011/11/10(木) 19:55:31.55 ] きさまら同じ話題を難解ループしてんだよｗ 318 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 20:20:19.96 ] お前もいつまでこのスレ読んでるつもりだ？ 319 名前：１３２人目の素数さん [2011/11/10(木) 20:33:33.69 ] 命ある限り読むつもりだよｗ その5辺りから読んでるんだから 320 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 20:34:33.65 ] その１からのログを保持してる俺はそろそろ飽きてきた 321 名前：１３２人目の素数さん [2011/11/10(木) 20:39:10.71 ] なぜなにスレッドの 洗濯小売はどうなったのか？ 322 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:44:01.56 ] >>316 では、今のロジシャンは何をやりたいの？ 323 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:47:13.21 ] ただのパズラー？ 324 名前：１３２人目の素数さん [2011/11/10(木) 22:58:40.05 ] 従来の論理学は コンピュータサイエンスに移ったよ。 洋書のCSシリーズのが充実している。 325 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:59:07.72 ] パズラーに失礼の無いように 326 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 09:49:01.53 ] 第二不完全性定理の証明がわかりません。具体的には、 PA|- Pr(【φ】)→Pr(Pr(【φ】)) をどうやって証明するのかがわかりません。 不完全性定理ってなかなか難しいですね。 327 名前：１３２人目の素数さん [2011/11/11(金) 19:49:22.09 ] 補題 Σ1文φについてPA|-φ→Pr(【φ】) 328 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 21:57:15.05 ] >>327 定義に関する帰納法で証明すればいいんですかね？ φが原子論理式のとき φが��Ψのとき φが、、、、 んーいまいちまだ分からないんですが。 329 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 22:14:05.71 ] たとえば PA|- ∀x∀y(x=y→Pr(【x=y】)) はどうやって証明するんでしょうか？ 330 名前：１３２人目の素数さん [2011/11/11(金) 22:56:20.05 ] >>329 PAの定義や証明体系に依存する。 331 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 01:49:07.93 ] >>330 たしかにそうですね、、、定義も書かずすみませんでした。 ところで、第二不完全性定理を証明する際に使われる導出性条件(derivability conditions)というのが３つありますよね。 D1 PA|- φ→Pr(【φ】) D2 略 D3 PA|- Pr(【φ】)→ Pr(【 Pr(【φ】) 】) このうちのD1とD3は何が異なるのでしょうか？ Pr(【ψ】)をD1のφとして考えれば、 D3はD1に含まれる気がするのですが。 332 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 03:39:12.71 ] D1が間違っているように見えるが、君の参考にしている本には本当にそう書いてあるかい？ 333 名前：１３２人目の素数さん [2011/11/12(土) 06:54:09.56 ] >>331 D1はPA|-φならばPA|-Pr(【φ】) だと思いますよ。 334 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 09:05:16.20 ] D1が間違っていました、失礼しました。 335 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 09:38:08.20 ] 次の論理法則を証明せよ：− 「前提が偽であることは帰結も偽であることを何ら保証するものではない。」 336 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 12:01:57.63 ] やばい数学オリンピック辞典見てみたけどさっぱり内容がわからない・・ 337 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 12:37:56.98 ] １ |-A←→B ２ |-A ⇔ |-B 1と2って同値でしょうか？ 338 名前：１３２人目の素数さん [2011/11/12(土) 13:28:48.48 ] １から２を示す。 |-A←→B |-A→B∧B→A |-A→B------(1) |-B→A------(2) もし|-Aなら(1)とMPで|-B、|-A⇒|-B もし|-Bなら(2)とMPで|-A、|-B⇒|-A よって |-A ⇔ |-B。 逆に２から１は一般に出ない。 339 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 16:46:34.16 ] >>338 助かりました、ありがとうございます。 340 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 17:06:01.89 ] >>269 ＞関数解析にとっても代数方程式は重要なの。 ＞整数論と関数解析は分けることができないの。 この屁理屈だと、数学と物理学も分けることができない、となる。 物理学にとっても、数学は重要であるからだｗ もちろん、他の学問でも同じことだが。 ＞向かう方向はおなじだから。 具体的に、どこだいｗｗｗｗｗｗｗ 341 名前：１３２人目の素数さん [2011/11/12(土) 21:19:30.75 ] >>340 どこが屁理屈なのかわからない 342 名前：１３２人目の素数さん [2011/11/12(土) 21:22:49.41 ] >>341 つまり、数学と物理学は分けることができない、と 343 名前：１３２人目の素数さん [2011/11/12(土) 22:55:45.50 ] 猫は？ 344 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 22:58:56.97 ] なにかと忙しいらしい 54: 11/09(水)21:06 AAS 猫がカンボジア国籍取得。五輪に前進。 57: 11/12(土)09:51 AAS 猫 五輪確定？カンボジア3選手が選考レース辞退 来年のロンドン五輪男子マラソンを目指し、カンボジア国籍を取得した猫が出場する五輪選考レース「東南アジア競技大会」(16日、ｲﾝﾄﾞﾈｼｱ)を出走予定の同国代表3選手が辞退｡同レースに出走する同国選手は猫のみになった｡ 345 名前：１３２人目の素数さん [2011/11/13(日) 05:08:28.07 ] >>342 数理物理学抜きの数学は考えられないな 346 名前：１３２人目の素数さん [2011/11/13(日) 10:25:14.55 ] >>345 数理論理学抜きの数学も考えられんよ 347 名前：345 [2011/11/13(日) 11:21:31.05 ] >>346 全く同意する。 数理論理学は数学の重要な分野だと思う。 348 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 11:54:52.99 ] ベン図さえあれば論理学いらん 349 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:00:45.38 ] 全く同意する。 アダルトビデオは映像芸術の欠くべからざるジャンルだ。 350 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:06:48.71 ] >>342 数学と物理の一部は分けられない。 でも、数学と論理学は分けられる。 数学と物理を僧侶と牧師に例えるなら 基礎論はただの禿げてる人。 見かけは僧侶に近いが考えていることは違う 僧侶と牧師は見かけは違うしスタイルも違うが 考えている方向性は同じ 351 名前：官軍（一兵卒）(＾o＾) mailto:sage [2011/11/13(日) 12:42:52.49 ] (Ｐ⊃Ｑ)⊃(¬Ｑ⊃¬Ｐ) は tautology であり。 “(ＰならばＱである)ならば、(ＱでないならばＰではない)”が成立する。 しかし、[Ｐ⊃(ＱＶＲ)]⊃[(Ｐ⊃Ｑ)Ｖ(Ｐ⊃Ｒ)] は tautology であるのに “ＰならばＱかＲであるならば、ＰならばＱかまたはＰならばＲである”は 成立しない。 352 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:44:46.23 ] ことがら Ａ，Ｂ，Ｃ，Ｄ が在り、これらについて次の２つの関係が成り立って いるものとする。 　　(ｲ) Ａであれば、Ｂか又はＣである。 　　(ﾛ) Ｄであれば、ＢでもＣでもない。 このとき、以下の主張 (1) 〜 (8) のうち正しいものを列挙せよ。尚、解法も述べよ。 　　(1) Ｄでなければ、Ａではない。 (2) Ｃであれば、Ｄではない。 (3) Ａでなければ、Ｄでないか又はＢではない。 (4) Ａでなければ、Ｄではない。 (5) Ｂでなければ、Ａでないか又はＤである。 (6) Ｂでなければ、Ａでないか又はＣである。 (7) Ｂであれば、Ｃではなく、Ｄでもない。　 (8) ［Ｂでなければ、Ｄではない］か又は［Ｄでなければ、Ｂではない］ 353 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 14:58:00.91 ] 結局、導出性条件(derivability conditions)の証明がわからず、第二不完全性定理もしっかり理解できなかった。 354 名前：１３２人目の素数さん [2011/11/13(日) 15:32:57.93 ] >>350 ＞数学と物理の一部は分けられない。 一部とは具体的に何を指すか？ もし「理論物理学」を指すならあなたが間違っている。 理論物理学は、物理であって数学ではない。 なぜなら理論物理学も物理現象を扱うからである。 理論物理学は数学のように証明によって その真偽が決まるわけではない。 355 名前：１３２人目の素数さん [2011/11/13(日) 15:37:15.51 ] >>350 ＞でも、数学と論理学は分けられる。 物理において数学が使われているように 数学において論理が使われているだけだ というのであれば、もちろん分けられる。 し・か・し、論理の数学的研究は、道具の使い方の研究ではない。 論理そのものの数学的構造を調べることにある。 したがって、数学の証明には全く役に立たないことは多々ある。 証明に役立たない論理の研究は無意味だというのは 物理に役立たない数学の研究は無意味だというのと 同程度に見識が狭い。 356 名前：１３２人目の素数さん [2011/11/13(日) 15:43:41.36 ] >>350 >（数学と物理は） >見かけは違うしスタイルも違うが >考えている方向性は同じ と思ってるなら数学も物理も分かってない。 数学では、ユークリッド幾何も非ユークリッド幾何も意味がある。 しかし物理学では、ニュートン力学と相対論の両方が意味がある、 ということはない。意味があるのは物理現象と整合する理論だけだ。 ちなみに、ニュートン力学の速度の合成はユークリッド的 相対論の速度の合成はクラインの円盤の変換として 実現できるので非ユークリッド的である。 357 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 15:53:35.40 ] >>356 物理学でも、 ニュートン力学と相対論は、両方意味があるよ。 状況に応じて使い分けられている。 358 名前：１３２人目の素数さん [2011/11/13(日) 15:56:21.05 ] >>350 >（基礎論は見かけは数学に近いが)考えていることは違う まず基礎論という言葉は論理学を指すものではないから 論理学という意味で言っているのならば、明確に間違っている。 さて、>>356で、「物理的世界」のように 「数学的世界」があるわけではないことを ユークリッド幾何と非ユークリッド幾何の 例で示した。 数理論理学の研究から、多種多様な数学の存在が示される。 もし、数学と物理は「唯一無二の世界」を探求する点で似ており、 論理学は「多種多様な可能世界」を想定する点で異なるというなら その人は、数学を誤解している。数学は「多種多様」なのであって 数理論理学はその事実を示しているに過ぎない。 359 名前：１３２人目の素数さん [2011/11/13(日) 15:58:14.42 ] >>357 ニュートン力学は単に「方便」として用いられているにすぎない。 非ユークリッド幾何もごく小さい箇所では、ユークリッド的であると みなせるのと同様な意味で、だ。 しかし、そのことは、ニュートン力学が 物理的に「正しい」ことを意味しない。 360 名前：１３２人目の素数さん [2011/11/13(日) 16:05:43.86 ] >>359 物理に正しいも間違いもないよ。 全てはモデルなんだから。 真実があるとしたら、それは神のみが知りうる。 それが物理学のとる立場だ。 大学生になったら、そういうことを意識してくださいね！ 361 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 16:35:17.23 ] >>359 ニュートン力学は、正しいよ。 通常の状態では、相対論と一致するとてもよい近似理論。 精度の高さと計算効率の良さから、今でも使われている。 というより、ほとんどニュートン力学だよ。 相対論が必要になるのは、かなり特殊な状況だ。 362 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 16:52:36.52 ] >>361 GPSで使うぞい 363 名前：猫 ◆MuKUnGPXAY mailto:age [2011/11/13(日) 18:28:46.96 ] 通常の場合、（どんな）物理理論にも適応限界が存在すると考えるのが 自然ですね。ソレは取りも直さず物理理論の正当性は（数学的な厳密性 ではなくて）実験結果との整合性に依って担保されるからであり、また 実験から得られる数値データには必ず誤差が含まれるという事実にも注 意が必要ですね。でも数学に於ける主張には如何なる適応限界も存在し ません。ソレは『その命題が成立する条件が全て明確にされてる』から ですね。 猫 364 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:33:16.64 ] >>361 相対論は電磁気学の一部だろ。電磁気学は認めない立場とかそういう特殊な方？ 365 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:34:41.32 ] 特殊相対性理論の方な 366 名前：１３２人目の素数さん [2011/11/13(日) 18:36:26.66 ] >>353 まずはΣ1完全性定理を ゲーデル数で算術化するところから考えよう。 367 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:46:39.06 ] >>364 電磁気学は、相対論の前に出来ていると思いますよ？ 相対論なしでも電磁気学はなりたつと思います。 もちろん相対論とも矛盾しないですが。 368 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 19:11:30.37 ] 数学わからない人は、マクスウェルの方程式と 特殊相対性理論の関係もわからないんですねえ。 369 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 20:09:28.34 ] 例えば磁場は相対論効果によるものだし、特殊相対論の原題は 「動いている物体の電気力学」で、電磁気学のうち取り扱いがいい加減だった 相対運動をする場合の理論なんだよ。 実は伸び縮みするとか結構どうでもいい話。 ウケがいいからクローズアップされるだけで。 370 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 21:38:20.80 ] 前の話を蒸し返すけど、物理なんかの測定から理論を抽出するところは逆数学じゃないの？ 逆数学にそういった応用例とかないのかしらん？ 371 名前：１３２人目の素数さん [2011/11/13(日) 21:57:42.68 ] そもそも逆数学じゃないそれ。 そーゆーのは「抽象」っていう。 372 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:01:47.42 ] ガウス？ 373 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:07:48.80 ] 逆数学とやらは知らんが、そんなガチガチにやっても絶対流行らん。 374 名前：１３２人目の素数さん [2011/11/13(日) 22:12:27.72 ] ここでまともに逆数学なんて語られていないから 参考にしないほうが良いよ。 375 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:35:30.31 ] >>366 形式化されていない��1完全性定理なら証明できました。が、形式化されたそれを証明する方法がよくわかりません。 ところで、私は前原先生の本をベースに勉強しています。 以下のページでは、前原先生の証明を土台にして第二不完全性定理を証明しているみたいなんですが、これって正しいですか？ miuse.mie-u.ac.jp/bitstream/10076/6295/1/AN100450900050008.PDF 376 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:38:53.70 ] >>375の追記 とくに定理12以降の部分についてです。これなら私にも理解できそうなんですが、 他の文献と比べて記述があっさりしている気がして本当に正しいのか不安に思ってしまいました。 377 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 00:39:36.38 ] 第二不完全性条件に関して質問をしている者です。 自分なりに考えてみたのですが、以下の証明って正しいでしょうか。 表現定理より、再帰的述語ならばPAで数値別に表現可能である。 r is recursive ⇒ PA|-R また、 PA|-R ⇒ PA|-Pr(【R】) は証明できる。 したがって、 r is recursive ⇒ PA|-Pr(【R】) また、証明できる論理式に対して仮定を増やしても、その論理式は証明できるので、 PA|-R→Pr(【R】) は証明できる。 ゆえに、 r is recursive ⇒ PA|-R→Pr(【R】) 378 名前：１３２人目の素数さん [2011/11/14(月) 01:18:05.53 ] >>377 間違えがある。 rが再帰的、つまり表現可能とは、 r⇒PA|-R ¬r⇒PA|-¬R の2つが満たされること。 rが再帰的⇒PA|-Rにならない。 そしてそのPDFは証明の誤りや脱字や 定義の足らない部分が多数含まれている、 読まないほうが良い。 379 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 05:08:59.80 ] ことがら Ａ，Ｂ，Ｃ，Ｄ が在り、これらについて次の２つの関係が成り立って いるものとする。 　　(ｲ) Ａであれば、Ｂか又はＣである。 　　(ﾛ) Ｄであれば、ＢでもＣでもない。 このとき、以下の主張 (1) 〜 (8) のうち正しいものを列挙せよ。尚、解法も述べよ。 (1) Ｄでなければ、Ａではない。 (2) Ｃであれば、Ｄではない。 (3) Ａでなければ、Ｄでないか又はＢではない。 (4) Ａでなければ、Ｄではない。 (5) Ｂでなければ、Ａでないか又はＤである。 (6) Ｂでなければ、Ａでないか又はＣである。 (7) Ｂであれば、Ｃではなく、Ｄでもない。　 (8) ［Ｂでなければ、Ｄではない］か又は［Ｄでなければ、Ｂではない］ 380 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 05:10:34.13 ] 論理法則とはそも何ぞや？ 381 名前：１３２人目の素数さん [2011/11/14(月) 08:52:14.54 ] >>380 そういうのは数理論理学ではなくて論理学がやることだね 382 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 09:15:32.61 ] >>384 数理論理学（＝記号論理学）と論理学とはどう違うのさ？　ヽ(^。^)ノ 383 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 10:16:00.81 ] 記号を使うかどうか 384 名前：１３２人目の素数さん [2011/11/14(月) 10:21:26.09 ] 「記号論理学」には「(アリストテレス流の)伝統的論理学」は含まれない。 385 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 14:53:23.90 ] >>380 ：１３２人目の素数さん：2011/11/14(月) 05:10:34.13 　　＞ ＞論理法則とはそも何ぞや？ 　　　論理法則＝トートロジー 386 名前：１３２人目の素数さん [2011/11/14(月) 18:44:59.32 ] ゲーデルオリの証明で不完全性定理アプローチしとんか モデル論使えば一発なんやけどな 387 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 19:42:18.19 ] ゲー・デルオリって誰 388 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 19:43:51.28 ] ゲロ出る俺 389 名前：１３２人目の素数さん [2011/11/14(月) 20:28:44.06 ] ゲーデルオリジナルの略にきまっちょるがな 390 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 21:55:34.44 ] 超素人なんだけど、ゲーデルの不完全性定理と対角線論法の関係を教えてくれ 何と何が対応しているんだ？ 対角線論法じたいは、数学ガールで分かった。しかし不完全性定理はあの本でもイミフだった。 391 名前：１３２人目の素数さん [2011/11/14(月) 22:14:05.98 ] 第1不完全性定理はPAの中の論理式で、 ¬を付けても付けなくても証明不可能なものが存在すると主張する定理。 この論理式はゲーデル文と言われ、対角線論法はゲーデル文をつくる際に必要。 対角化定理(不動点定理)自体は数学のあらゆる場所に登場する。 チューリング機械の停止判定問題が否定的に解ける件などもこれが原因。 392 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 23:01:20.98 ] >>389 ヴェルタース・オリジナルみたいなもん？ 393 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 00:22:52.63 ] >390 「不完全性定理と対角線論法の関係」という話だと、もうちょっと突っ込んだ考えが必要。 Webだとこれが良くまとまっていると思う。 (pdf)自己言及の論理と計算 ttp://www.kurims.kyoto-u.ac.jp/~hassei/selfref2006.pdf 394 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 01:46:48.53 ] >>378 >間違えがある。 >rが再帰的、つまり表現可能とは、 >r⇒PA|-R >¬r⇒PA|-¬R >の2つが満たされること。 >rが再帰的⇒PA|-Rにならない。 仰る通りです。私が間違ってました。 >そしてそのPDFは証明の誤りや脱字や >定義の足らない部分が多数含まれている、 >読まないほうが良い。 たしかに、題からしてすごい間違いを犯してますね。 ただ、私の気になる第二不完全性定理の箇所に関しては、私には誤りが見つかりませんでした。そして、非常に分かりやすい証明でした。 具体的にどこが誤っているか教えていただけませんか？ よろしくお願いします。 395 名前：１３２人目の素数さん [2011/11/15(火) 07:24:03.09 ] >>392 知りません/// >>393 良くかけてるとおもう >>394 誤りがあるか否かが問題ではない 誤りがると信じるか否かが問題である 396 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 14:45:36.71 ] 言及されてる論文も貼っとく。 www.springerlink.com/content/h881p406u0378850/fulltext.pdf 397 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 21:28:16.27 ] >>390 www.age.ne.jp/x/eurms/GDL.html#00 398 名前：１３２人目の素数さん [2011/11/15(火) 22:03:40.15 ] >>338 >逆に２から１は一般に出ない。 具体的な反例は？ 399 名前：394 mailto:sage [2011/11/15(火) 22:57:44.24 ] >>395 そうですか、残念です。 もう少し考えてみます。 400 名前：１３２人目の素数さん [2011/11/15(火) 22:58:52.36 ] 演繹定理から逆も成り立つ＾＾； 401 名前：１３２人目の素数さん [2011/11/15(火) 23:01:53.16 ] >>363 数学についてはもちろんおっしゃるとおりですが，物理理論にとって実験結果 との整合は実は単なる結果であって，その理論の単純さや美しさこそが正当性 の根拠なのではないでしょうか（たとえば特殊相対論）． そろそろ２１世紀の科学哲学が必要なのでは？ 402 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:07:07.64 ] 実験との整合性は物理理論の目的 特殊相対性理論では、マイケルソン・モーリーの実験の意味を考えるのが、 アインシュタインの研究の動機。 403 名前：１３２人目の素数さん [2011/11/15(火) 23:17:36.97 ] >>402 知ってのとおり天動説だって観測との整合性はあった． アインシュタインはマイケルソンモーリーの実験を知らなかったという 説もある（それは十分あり得ることだろう）． このあたりはこの板のみなさんにはいうまでもないだろうが． 404 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:21:18.86 ] 俺が彼氏にフェラチオしてるときはもっと激しくジュパジュパ音を出してあげてるよ 405 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:22:45.71 ] 理論が美しい、とか誰が判定するんだ？ 406 名前：１３２人目の素数さん [2011/11/15(火) 23:27:08.83 ] >>405 単純さなら，相当程度客観的に評価できるんでないかい． 407 名前：１３２人目の素数さん [2011/11/15(火) 23:37:59.91 ] >>399 本当に間違っているか不明。 余り信じないほうが良い。 ゲーデルの証明は複雑で、粗探しは大変そう。 そのPDF書いた人もself-containedじゃないと ことわりを入れてるのでなおさら難しい...。 不完全性定理は有限の立場、つまり2項述語∊を使ってよいなら、 集合論を経由してかなりシンプルに証明できる。 408 名前：１３２人目の素数さん [2011/11/15(火) 23:38:50.87 ] 訂正： 不完全性定理は有限の立場、 ↓ 不完全性定理は有限の立場を出て、 409 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:43:22.09 ] >>400 演繹定理って、 Γ,A|-B ⇒ Γ|-A→B のことだよね？ Γ|-A ⇒ Γ|-B とは、違うのでは？ 410 名前：１３２人目の素数さん [2011/11/15(火) 23:54:38.09 ] >>409 |-A⇔|-B を仮定。 |-A⇒|-B について考えると、 |-A より {B}|-A 演繹定理を使って |-B→A-------(1) 逆に|-B⇒|-A について考えると、 |-A→B-------(2) (1),(2)から |-A←→B　　　　　　　　　　□ 411 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:58:26.37 ] >>407 真摯なコメントありがとうございます。 >不完全性定理は有限の立場、つまり2項述語��を使ってよいなら、 >集合論を経由してかなりシンプルに証明できる。 様相論理を使う証明のことですか？ もう導出性条件の有限な証明を理解するのは諦めようかな、、、。 412 名前：１３２人目の素数さん [2011/11/16(水) 00:06:41.74 ] >>410 まちがっとるやろ． それは，|-Aかつ|-Bから|-A←→Bを出しとるんや． 413 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 00:07:10.52 ] >>410 >|-A より {B}|-A ここは、 |-A⇒|-B より、 {B}|-A⇒|-B としか、言えないのでは？なので、以下も >演繹定理を使って >|-B→A-------(1) |-B→A⇒|-B としか言えないと思いますが。 414 名前：410 mailto:sage [2011/11/16(水) 07:10:46.56 ] >>412-413 完全に間違っていた 415 名前：１３２人目の素数さん [2011/11/16(水) 07:50:18.61 ] >>411 公理的集合論を使った証明ですね。 補題：集合論は集合モデルの存在を証明できない、 を使ってPAの第2不完全性を証明。 第1はRE集合での証明がシンプルで見通しが良い。 詳細な論理式についての議論を省ける。 ただし集合が胡散臭いなら無理...。 416 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 19:33:17.57 ] 確かに今じゃ数理論理学は、哲学方面のほうが盛んだよな。 クリプキの定理とか数学史を塗り替えるものだし。 417 名前：１３２人目の素数さん [2011/11/16(水) 20:22:30.89 ] 394さんの質問にお答えします。 まず関係というからには「何に関する何項関係か」を明示する必要があります。 　例：「nは素数である」は数nに関する１項関係である。n+3<m は数n,mに関する２項関係である。 そしてたとえば「数 n,m に関する２項関係が論理式Aによって表現される」という場合には、 A中に n,m に対応する自由変数記号 x,y があって、x,y に「数n,mを表す項」を代入した論理式のことを 論じる必要があります。 そこで件の悲惨なPDFですが、たとえば89ページの下から4〜3行目の 　定理11より、関係 Bew(「r」) は論理式 bew(『r』) によって表現される。 という部分に次の質問をすれば簡単に終わりかと思います。 関係 Bew(「r」) は何に関する何項関係ですか？ 論理式 bew(『r』) 中の対応する自由変数記号はどれですか？ （注意：83〜84ページにあるように『r』は定数を表す項であって自由変数記号を含みません） 418 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 22:19:31.52 ] >>417 解説ありがとうございます。 納得しました。たしかに、皆様の仰る通り、このpdfは間違いがけっこうありました。たとえば、 他にも、pp91の(15.6)から(15.7)にかけての箇所も誤りですよね？ 417さんのおかげで、より深い理解が得られました。ありがとうございます。 419 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 22:31:12.25 ] >>417 追記 もし、第二不完全性定理の証明について解説しているネット上の資料をご存知でしたら、教えていただけませんか？ 言語は英語でも構いません。それと、証明の方法は、様相論理等によるものではなく、第一不完全性定理の証明を形式化してする証明によるものでお願い致します。 、、、なんかものすごい厚かましいですね、すみません。 420 名前：１３２人目の素数さん [2011/11/17(木) 00:13:52.72 ] ttp://www.scribd.com/doc/51607996/An-Introduction-to-Godel-s-Theorems ttp://phil.gu.se/logic/uppsatser/blanck_logd.pdf 余談だが可証性述語を様相演算子に置き換えることで、 第2不完全性定理は証明できない。 そもそもの3つの可導性条件を満たすことを示すのが この証明の最大の難所なわけで、これは第1不完全性定理の 算術化を避けては通れない。 しかしこの算術化を厳密に行うテキストはほとんど皆無で、 大抵は3つの条件を事実として認めるか、アウトラインを述べるにとどまる。 かつてNatarajan Shankarは定理自動証明機械を用いて完全な証明を試みたが、 そのプログラム中にはエラーが発見された...。 またBoolosははじめから様相論理で算術を展開したが、 これは強い体系のため、第2不完全性定理よりも弱い定理になることが指摘されてしまう...。 421 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 04:41:25.90 ] 次の問題にこたえよ。　解答のみならず、解法も記せ。 【問題】ことがら Ａ，Ｂ，Ｃ，Ｄ があり、これらについて 次の２つの 　　　　関係が成り立っているものとする。 　　　　　（ｲi Ａであれば、Ｂか又はＣである 　　　　　（ﾛ）Ｄであれば、ＢでもＣでもない 　　　　　　　　　 　　　　　このとき、以下の主張（１）〜（７）のうち正しいものを列挙せよ。 　　　　　　（１）Ｄでなければ、Ａではない 　　　　　　（２）Ｃでなければ、Ｄではない 　　　　　　（３）Ａでなければ、Ｄでないか又はＢではない 　　　　　　（４）Ａでなければ、Ｄではない 　　　　　　（５）Ｂでなければ、Ａでないか又はＤである 　　　　　　（６）Ｂでなければ、Ａでないか又はＣである 　　　　　　（７）Ｂであれば、Ｃではなく、Ｄでもない 、 422 名前：１３２人目の素数さん [2011/11/17(木) 11:19:21.45 ] スレチ 論理学スレか質問スレでやれ 423 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 15:35:49.54 ] いちいちコピペに反応するな 424 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 16:31:46.49 ] >>420 参考資料と解説ありがとうございます。資料は後ほどじっくり読んでみたいと思います。 やはりderivability conditions の証明は相当に難しいのですね。 すみません、まだ疑問があります。以下の推論はどこがおかしいでしょうか。以下を認めるとD1からD3がでてきてしまうのですが。 D1より PA|- A ならば PA|-Pr(【A】) また、 PA,A|- A ゆえに、 PA,A|- Pr(【A】) 演繹定理より、 PA|- A→ Pr(【A】) 425 名前：１３２人目の素数さん [2011/11/17(木) 18:39:44.83 ] >>424 ＞PA|- A ならば PA|-Pr(【A】) ＞また、 ＞PA,A|- A ＞ゆえに、 ＞PA,A|- Pr(【A】) ここがおかしい。 PA,A|-A のとき、 A|-A かつ PA|-/-A があり得る。 426 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 19:38:25.07 ] >>425 >PA,A|-A のとき、 >A|-A かつ PA|-/-A があり得る。 すみません、、まだよく分からないのですが、 PA|-/-Aのときは、Prの定義より、PA,Aから Pr(【A】)は証明できないということでしょうか。 427 名前：１３２人目の素数さん [2011/11/17(木) 19:58:19.69 ] >>426 証明の前にわかっていること。 PA|-A が成り立つとき、PA|-Pr(【A】) を結論してよい。 証明の仮定。 PA,A|-A 例えばAがPAから独立とする。 するとPA|-/-A。 このとき、PA|-Pr(【A】)もしくはPA|-/-Pr(【A】)。 ここで、PA|-/-Pr(【A】)の場合を考える。 すると、A|-Pr(【A】)もしくはA|-/-Pr(【A】)。 さらに、A|-/-Pr(【A】)の場合を考えると、 PA,A|-/-Pr(【A】) 428 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 21:36:37.32 ] >>427 よくわかりました。丁寧な解説ありがとうございます。 429 名前：１３２人目の素数さん [2011/11/17(木) 23:01:37.14 ] >>428 ほんとにわかった？ Pr述語が途中ですり替わっているだけでしょ？ 424はきちんと書けば、つぎのようになるでしょ。 D1より PA|- A ならば PA|-Pr( PA,【A】) また、 PA,A|- A ゆえに、 PA,A|- Pr( PA+A,【A】) 演繹定理より、 PA|- A→ Pr( PA+A,【A】) つまり、この最後が　Pr( PA,【A】)　でなければD3は出てこないでしょ？ Pr( PA+A,【A】)　はまあ自明だよね。 430 名前：官軍（一兵卒）(＾o＾) mailto:sage [2011/11/18(金) 02:03:43.06 ] >>424 ＞演繹定理より ﾜﾛﾀYO 431 名前：１３２人目の素数さん [2011/11/18(金) 14:31:35.38 ] 電波テロ装置の戦争(始) エンジニアと参加願います公安はサリンオウム信者の子供を40歳まで社会から隔離している オウム信者が地方で現在も潜伏している それは新興宗教を配下としている公安の仕事だ 発案で盗聴器を開発したら霊魂が寄って呼ぶ来た <電波憑依> スピリチャル全否定なら江原三輪氏、高橋佳子大川隆法氏は、幻聴で強制入院矛盾する日本宗教と精神科 <コードレス盗聴> 2004既に国民20%被害250〜700台数中国工作員3〜7000万円2005ソウルコピー2010ソウルイン医者アカギ絡む<盗聴証拠> 今年５月に日本の警視庁防課は被害者SDカード15分を保持した有る国民に出せ!!<創価幹部> キタオカ1962年東北生は二十代で2人の女性をレイプ殺害して入信した創価本尊はこれだけで潰せる<<<韓国工作員鸛<<<創価公明党 <テロ装置>>東芝部品)>>ヤクザ<宗教<同和<<公安<<魂複<<官憲>日本終Googl検索 432 名前：１３２人目の素数さん [2011/11/18(金) 16:17:35.18 ] 魂は幾何学 誰か(アメリカ)気づいた ソウルコピー機器 テロ装置の再読願います 433 名前：１３２人目の素数さん [2011/11/18(金) 22:31:02.80 ] 数学、特にその中核となる数論は、 古代の人、未来の人、遠い外国の人、もしかしたら 宇宙人とさえも交信可能な、コミュニケーション素材。 でも基礎論は今の限定された人々のあいだだけだな。 434 名前：１３２人目の素数さん mailto:sage [2011/11/18(金) 22:33:47.42 ] 虎の威を借る狐 って言葉知ってるか？ｗ 435 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 02:57:04.13 ] 通常の整数ではなく、代数的整数でも宇宙人と交信可能だというわけか。 代数的整数の定義は、必然的に選ばれたものだとでも？ 436 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 19:12:38.48 ] RのQ-線形空間としての基底は存在するが、それを「具体的に構成して見ることは出来無い。」を証明するにはどんな枠組、手法が要るの？ 437 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 20:30:32.85 ] 選択公理とパラレルになってる 438 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 02:47:31.19 ] 選択公理の成り立たないモデルを作る必要がある罠 439 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 09:46:17.55 ] >>433 自然数も実数と同様に人の作ったウソである 440 名前：１３２人目の素数さん [2011/11/23(水) 10:13:50.48 ] >>439 ウソという言葉に否定的なニュアンスを勝手に感じてはならないわけですね。 441 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 11:09:09.69 ] イヌやサルにとって自然数も実数もまったく必要がないものである． 442 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 12:34:43.78 ] イヌヤサルは物を数えるのに自然数は用いていないちう主張？ 443 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 12:44:02.85 ] 1,2,3,∞ 444 名前：１３２人目の素数さん [2011/11/23(水) 13:35:33.45 ] 数学はつまるところ数量の科学でしょ？といったら笑われたｗ 構造・作用・空間の科学だと。 でもそういう概念も数量記号化不可能なものなら数学ではないんじゃ・・・ 445 名前：１３２人目の素数さん [2011/11/23(水) 13:37:34.74 ] 数量的概念のはいらない数学なんてありうるのでしょうか？ あったとしてもそれはある公理系をもった記号論理学にすぎなくなるのでは。 446 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 14:18:31.81 ] >439 そうすると類別も対応も嘘になるから何にもできなくなると思う。 447 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 14:55:53.34 ] 嘘、というか、都合のよいフィクション 448 名前：１３２人目の素数さん [2011/11/23(水) 15:12:46.43 ] 自然数全体の集合というのは、便宜的なものにすぎないが、 自然数に対する興味は知性的な頭脳集団の存続する限り 残るだろう。 素数はどれくらいあるか？(リーマン予想) 不定方程式に整数解はあるか？(フェルマー予想) そして素晴らしいことには、この二つの問いには 19世紀以来、継続的に散発的でない進展があるということ。 449 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 15:17:52.53 ] ただし、数論と比較して、幾何学は、 もともとの意味の幾何学(クライン以前)は、継続的な進展は途絶え、 数学としての深みのある問題はなくなってしまったので、 数論の進展も永久に残るかどうかは分からない。しかし、 それは数学ないし知性自体の死を意味するかもしれない。 450 名前：１３２人目の素数さん [2011/11/23(水) 15:49:07.89 ] 最近集合論を勉強しているけど 座標を前にしてRの直積、写像、ベキ乗について考えてるとなんだか わけがわからなくなってくる。それぞれが原子、運動、空間の範囲 みたいに見えてくる。しかしそうするとそもそも集合って何って思え てきて頭が死ぬ！ 451 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 16:13:15.63 ] その程度で死ぬ頭ならそのまま死んだ方がいい 452 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 17:29:15.38 ] >>449 「クライン以前の幾何学」（初等幾何）というのは 「ガロア以前の代数学」（初等代数）というのと 同程度の意味しかない。 クライン以降、幾何学はリー群論に進化してしまった。 453 名前：１３２人目の素数さん [2011/11/23(水) 17:34:03.03 ] >>450 ある人に、集合とは何か？と聞かれたので、 「｛｝と，だけで表わせるもの」 と答えてやった。 {},{{}},{{},{{}}},･･･ 上記の最初の３つの集合は、それぞれ 自然数の０，１，２に対応する。 454 名前：１３２人目の素数さん [2011/11/23(水) 17:37:59.01 ] >>446 ＞そうすると類別も対応も嘘になるから どうも私の発言を誤解しているようだが、 私は０とか１とか２とかいう数がウソ（つまりフィクション） だといったのではない。 それらをひっくるめた概念としての自然数というものが ウソ（つまりフィクション）だといったのである。 例えば数学的帰納法というのは、あくまで願望にすぎない。 455 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 17:39:28.89 ] 数学は小説と同じ 人間の思考パターンの表現 数学が研究しているのは、脳という神経組織の振る舞い。 456 名前：１３２人目の素数さん [2011/11/23(水) 18:03:22.65 ] >>453 可視化へ進みすぎじゃあないか 前に少しグラフを習ったので、それだと考えると「見える」んだけどなあと思った。 つまり座標成分を点、写像は線と考えればいい。（完全）二部グラフならそれぞれの数が そのまま一致する。特に意味が無いけど、、 457 名前：１３２人目の素数さん [2011/11/23(水) 18:08:30.09 ] >>453 それは余り説明になっていない。 それにその書き方は一部の集合論の流儀にすぎない。 458 名前：１３２人目の素数さん [2011/11/23(水) 18:38:53.26 ] >>456 点と線で視覚化できる集合写像はごく一部にすぎないけど。 459 名前：１３２人目の素数さん [2011/11/23(水) 18:59:57.61 ] >>457 まあいいじゃん、聞いてきた相手もちゃんとした説明が欲しいんじゃないだろうし。 460 名前：１３２人目の素数さん [2011/11/23(水) 20:44:22.77 ] >>452 まぁ、ある意味そう言うこと。 しかし数論の場合は、ガロア以前の問題を ガロア以後の研究が解決し続けているのに対し、 幾何学は、問題自体を捨て去った。 捨てずに追いかけ続けたのが、和算。 日本人の性質を表しているようだ。 因みに幾何学という語が日本で使われ出したのは 明治以降。 461 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 21:05:08.00 ] 初等幾何学が研究されなくなったのは、 難しい問題がなくなったからではない。 難しい問題の全てが解決されないか、 解決されても散発的な解法しか発見されなくなったから。 462 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 21:07:40.13 ] 最近解かれたケプラー予想は初等幾何の問題。 そういう意味では進展は無いわけではないし 研究も全くなくなったわけではない。 しかし、発見された解法はどれも美しくない。 463 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 23:27:01.85 ] 現実と虚構をわざと混同させる意図のもと構成されたフィクション。 464 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 06:33:55.54 ] >>460 ＞幾何学は、問題自体を捨て去った。 とは思わんね。幾何学を合同変換群における不変式論と 定義しなおしてしまった時点で、不変式かどうか判定 すればすむ問題は、もはや問題ではない。 465 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 06:39:59.15 ] >>457 残念だが、ZFCでは集合論に集合以外のものは出てこない。 つまり{}と,以外で書き表さねばならないようなものは出てこない。 もちろん、内包的な定義は存在する。 しかし、これを外延的に表わせたとするなら やはり{}と,しか出てこない。 自然数であれ実数であれ複素数であれ、集合である。 すべて{}と,で表わせる。面倒だから省略記法で誤魔化してるだけだ。 466 名前：１３２人目の素数さん [2011/11/24(木) 07:01:01.81 ] >>465 一部の集合論がZFCだって言ってるんだけど。 467 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 07:07:32.62 ] >>466 一部というには、大きすぎるような。Axiom of Foundation が特殊 といいたいということでも、ちょっとなぁ。 468 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 07:43:18.26 ] 内包公理さえうまく定義すれば集合なんてブラックボックスでも形式化できる。 しかし{}と,だけで書けるってのおかしい。 非可算無限個の集合を紙の上にかけるなら元々ZFCなんていらないし。 469 名前：１３２人目の素数さん [2011/11/24(木) 10:43:13.01 ] >>464 初等幾何の全ての問題が捨て去られたわけではないね。 ケプラー予想などを除く最も主要だった問題群は、 今や代数幾何学という分野名で数論と密接に関連して 研究され続けていると。 470 名前：１３２人目の素数さん [2011/11/24(木) 11:00:32.48 ] しかし数論の問題と違って、幾何学は、 問題を昇華する過程で、結局古典的問題は 原型をとどめたままでも面白いものは無くなり、 結局捨て去られてしまったのだと思う。 円を有限分割して同体積の正方形に できないことは、まだ証明されてから 一世期たっていないはずだが、 ケプラー予想ほどではないけど、あまり評価されてないと思う。 471 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 11:34:46.08 ] 19世紀クラインは、幾何学の問題を不変式論に 還元したというより、群や不変式という 代数学の言葉を使って、幾何学の意味の 拡大を行ったというほうが正しいだろう。 それまで幾何学と思われなかったことまで 幾何学という言葉で綺麗にくくれると。 16世紀にデカルトがすでにユークリッド幾何学を 方程式論に還元できることは言っていた。 しかし、それでも和算家は、 幾何は幾何として研究していたわけで。 472 名前：１３２人目の素数さん [2011/11/24(木) 13:37:31.72 ] つまんねぇの。 473 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:26:00.68 ] 第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、 その場合は証明の定義を変更する必要があると 474 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:27:11.10 ] >>473 ミスしました。 第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、 その場合は証明の定義を変更する必要があるとwikipediaにはあります。 しかしそれでは定理の一般化とは言えないのではないでしょうか？ 475 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:35:59.28 ] wikipediaじゃ数学の勉強にはならん。 証明読め。 476 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:38:22.54 ] >>475 新井敏康の本では証明の定義を変えているという訳ではないようです。 wikipediaの記述が間違いなのでしょうか？ 477 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:50:53.34 ] なぜわざわざω無矛盾にしたのだろうかという考察が岩波文庫の不完全性定理本にある。 478 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:26:01.91 ] >>474 証明の定義というより可証性述語の定義。 今新井の本をちらっと見たけど 第一不完全性定理の証明の前に 算術化を行ってProv(a,b)を定義していて、 第一不完全性定理でロッサー述語を一気に導入して証明してた。 ロッサー述語は定理の条件のω無矛盾が無矛盾に広げられる。 ゲーデルも論文出したときは無矛盾にしたかったらしいよ。 479 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:30:45.57 ] >>478 ということは、純粋な一般化ということでいいのでしょうか？ 証明の中でPrの定義を変更していますが、証明する事柄にPrは現れないので。 480 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:13:54.22 ] ゲーデルとロッサーの原論文を読めばすぐに済むことをわざわざ質問する意図がわからない。 481 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:15:53.77 ] ゆとり世代なめるなよ 482 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:37:03.43 ] >>479 純粋な一般化とは何だろうか？ 483 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:41:54.66 ] >>482 「ω無矛盾な公理系には証明も反証も不可能な論理式が存在する」という定理を 「無矛盾な公理系には証明も反証も不可能な論理式が存在する」という形に一般化されますが、 この時の「証明」の定義は前者と後者で別物なのでしょうか？ 新井敏康「数学基礎論」を読む限りでは両者における「証明」の定義は同じ物のようですが、 484 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:43:16.48 ] というかそういう疑問を抱く時点で両者の証明を理解してない。 485 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:51:41.38 ] 対角線論法と不完全性定理は何と何が対応しているんだ？ 486 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:56:15.96 ] ゲーデルの完全性定理、不完全性定理の証明は面倒ではあるけど難解ではないからちゃんと読めよ。 それが解れば周辺論文もそんなに難しくないことがわかる。 広中やワイルズやペレルマンの論文よりずっと読みやすいぞ、内容も平易だし。 487 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:57:58.47 ] >>485 証明を読めば解る 488 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:06:24.94 ] >>483 同じ。 >>485 対角定理で証明も反証もできない論理式をつくる。 489 名前：483 mailto:sage [2011/11/24(木) 22:08:54.76 ] >>488 ありがとうございます! 490 名前：483 mailto:sage [2011/11/24(木) 22:18:31.37 ] 何度も申し訳ありません。 もうひとつわからない部分があります。 新井敏康「数学基礎論」においてderivability conditionsのうちの (D2)Pr(【A→B】)∧Pr(【A】)→Pr(【B】) を証明してありますがよく分かりません。 考えている公理系をPAというものとして、PAの標準モデルが存在することを用いて 原始再帰的関数の問題に帰着させて証明するのではいけないのでしょうか？ 491 名前：483 mailto:sage [2011/11/24(木) 22:25:25.50 ] >>490 (D2)PA|-Pr(【A→B】)∧Pr(【A】)→Pr(【B】)です。すみませんでした。 492 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:31:42.84 ] ここまでくると何で理解できないのかが理解できない 教科書を燃やして数学を勉強するのを諦めた方がいい 493 名前：１３２人目の素数さん [2011/11/24(木) 22:41:44.91 ] >>490 よく言っていることが理解できないけど それで証明できるなら別に良いと思う。 494 名前：１３２人目の素数さん [2011/11/24(木) 22:44:30.60 ] >>486 比べるんじゃない。 価値が全然違う。 495 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:44:33.77 ] 内容をキチンと吟味せず結果だけ質問しても何にもならないよ。 496 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:45:45.54 ] >>494 価値なんぞ較べてないだろ 難易度が違うと言っている。 497 名前：１３２人目の素数さん [2011/11/24(木) 22:49:20.70 ] そんなかじゃペレルマンのが圧倒的に難解だろうな 498 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:00:28.77 ] 予備知識のあるなしによるが内容の前提が一般数学の知識内におさまらない分 ペレルマンのが一番難解かもね。 それに較べたら予備知識ほぼゼロでも理解できるんだからゲーデルの論文なんて 有り難すぎて涙が出るくらいだ。 499 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:19:46.19 ] ゲーデルの論文ひいては数理論理学は数学ではない（から素人でも理解しやすい）、という可能性は？ 500 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:24:52.14 ] 理解しやすくはない、ゲーデルは証明は厳密詳細にやってるから、全て理解するのは面倒くさい。 でもあれが数学の証明でないなら、俺は数学の証明を読んだことがないな。 あれくらい諄い数学の証明はそうそうないぞ。 501 名前：猫にコネは不必要 ◆MuKUnGPXAY mailto:age [2011/11/25(金) 00:20:49.81 ] 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫 502 名前：１３２人目の素数さん [2011/11/25(金) 00:22:29.22 ] 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 芳雄 503 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 07:12:33.12 ] >>474 wikipediaにちゃんと 「命題の証明より小さな、否定命題の証明が存在しないという性質を追加」 って書いてあるじゃん。これが(ロッサーの方法の)全てだよ。 ところで、「矛盾の証明が存在しない」はPAで証明できないが 「すべての矛盾の証明について、 　これより小さな矛盾の否定の証明が存在する」 はPAで証明できる。もし「矛盾の証明が存在しない」ならば確かに 「すべての矛盾の証明について、 　これより小さな矛盾の否定の証明が存在する」 が、逆は真ではない。したがって、このことは、第二不完全性定理に 何ら疑念を生じさせるものではない。 504 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:37:39.57 ] >>500 それは君の数学の経験が浅いだけ。 505 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:43:33.93 ] >>499 そうだね。 高校数学すらほとんど使っていない。 帰納法くらいか。 数学というよりパズル。 506 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 09:21:51.82 ] >>503 しかし僕の持っている本では証明の定義は変えてありません。 あくまで定理を示す中で証明可能性述語を変形したものを 用いるのみで、定理のステートメントにおける「証明」の定義は ゲーデルのものとロッサーのもので 変わっていません。 507 名前：１３２人目の素数さん [2011/11/25(金) 10:02:59.16 ] >>506 その「持ってる本」を明示しなよ。伏せる必要ないだろ？ 508 名前：483 mailto:sage [2011/11/25(金) 11:00:01.17 ] >>507 新井敏康「数学基礎論」です。 509 名前：１３２人目の素数さん [2011/11/25(金) 22:01:31.69 ] >>465 それは通常ｎ番目の自然数と解釈されるような 推移的集合しか記述しない。 510 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 22:15:17.39 ] \ 511 名前：１３２人目の素数さん [2011/11/25(金) 22:51:17.77 ] >>506 定理で示される証明と 可証性述語が表現する証明はちげーよ 512 名前：483 mailto:sage [2011/11/26(土) 00:51:08.93 ] >>511 それでは>>483において両者の「証明」の定義は同じということで良いのですか？ 513 名前：１３２人目の素数さん [2011/11/26(土) 01:04:28.23 ] たりめー 可証性述語はその証明も反証もできない論理式探すためのどーぐ 何を意味してるかなんてかんけーねー 514 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 02:50:11.55 ] >>504 車種・車メーカー板に居る人？ 515 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 16:29:29.28 ] >>506 ＞あくまで定理を示す中で証明可能性述語を変形したものを用いる 「その変形を、新しい証明の定義とする」と読めない奴は池沼。 516 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 18:33:06.39 ] ゲーデルの第二不完全性定理の証明は、何をもって、証明されているか ということが問題なのだ。いかなる本にも、証明は書いてないのだ。 このような、方法で、証明ができるということが書いてあるのだ。 この違いは専門家とよく話さないとわからないもので、このような ところで説明されてわかることではない。 517 名前：１３２人目の素数さん [2011/11/26(土) 20:07:34.59 ] ゲーデルの第二不完全性定理の証明ごときで 専門家と話す事なんかない。 数学としてはエレメンタリーな組み合わせ論の証明にすぎない 518 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:09:09.83 ] 哲学や論理学としてみたら一流の結果かもしれないが、 数学としてみたら二流以下の結果 519 名前：１３２人目の素数さん [2011/11/26(土) 20:21:06.16 ] 平方剰余の相互法則のような、いつまでも高いレベルでの一般化があるようなよい定理だと思うが。 520 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:51:50.70 ] 平方剰余の相互法則の一般化の様に豊かな応用が無い。 521 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:55:04.45 ] 平方剰余の相互法則は、フェルマー予想界隈の 研究からの要請があって、一般化されてきたのであって、 単にいじくりまわしていたわけじゃ無い。 522 名前：１３２人目の素数さん [2011/11/26(土) 21:04:32.09 ] >>515 証明の定義自体は何もかわってないはず。 523 名前：１３２人目の素数さん [2011/11/26(土) 21:07:30.84 ] >>516 一応新井の本には証明が全部入ってる。 ただし冪関数ありのPAだけど。 524 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 21:39:39.54 ] >>523 ３章を読み終わっているなら聞きたいんだが、 P101の補題3.3.2は証明になっていないと思うんだが、どう？ 525 名前：１３２人目の素数さん [2011/11/26(土) 21:54:48.30 ] >>521 それは出鱈目が過ぎる 526 名前：１３２人目の素数さん [2011/11/26(土) 22:01:08.85 ] >>521 どう？ 527 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 22:02:04.34 ] 訂正 >>525 どう出鱈目？ 528 名前：１３２人目の素数さん [2011/11/26(土) 22:54:15.96 ] >>527 フェルマー予想界隈の「要請」から一般化されたとか歴史的におかしいだろ。 529 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:14:52.57 ] 第二不完全性定理をどこまで弱い算術で 証明できるかという方面の研究はあるよ まあ割と些事だけどね でも518はどうせP=?NP問題とかも 数学としてはエレメンタリーな二流の問題とか言って 切って捨てるんだろうな 530 名前：１３２人目の素数さん [2011/11/26(土) 23:25:41.21 ] >>524 確かに何をやっているのか理解できない。 「でよい。　　■」って何だよｗ 531 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:37:03.89 ] >>528 平方剰余の相互法則の重要な応用として、 全ての整数が四つの平方数の和で表されるという定理がある。 この種の問題(フェルマー予想はp乗数の和の問題)を初めとして 重要な応用を目指して一般化されてきた。 無目的に一般化してきたわけでは無い。 532 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:39:27.44 ] >>529 前半。些事、そうですね。 後半。それは解けてみてからでなくては わからないけれど、今までの状況からすると その可能性はかなり高いですね。 533 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 00:02:56.01 ] >>530 やっぱりそうだよね。 どうも破綻していると思えてならない 534 名前：１３２人目の素数さん [2011/11/27(日) 00:42:06.34 ] >>531 ルジャンドルによる四平方定理の証明は1770年。 平方剰余の相互法則を証明したガウスが生まれる前のこと。 535 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:18:37.60 ] >>534 それって証明に不備があったやつでしょ？ 19世紀にディリクレが埋めたけど。 536 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:21:34.41 ] とにかく平方剰余の相互法則の応用でそのルジャンドルの定理も 証明出来るし、相互法則の一般化でより深い整数論の定理がいろいろ証明できるのよ。 537 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:44:25.69 ] もひとつ補足しておくと、 平方剰余の相互法則は、何も無いところから いきなりガウスが見つけたものじゃなくて、 ルジャンドルの平方和の研究の中に その芽があるんです。相互法則のステートメントで 使うカッコをルジャンドル記号と言うでしょ。 538 名前：１３２人目の素数さん [2011/11/27(日) 04:00:55.62 ] >>537 相互法則を発見したのはオイラーじゃなかったっけ？ 539 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 05:41:22.25 ] >>523 普通の数学の定理と異なっている内容であることに気がついていない 証拠なのだ。 第一不完全性定理とは、全く性質が異なっていることに気がつくべき なのだが、普通気がつかない。 540 名前：１３２人目の素数さん [2011/11/27(日) 06:17:01.75 ] >>539=>>516かい？ 思わせぶりなことを書いても、2chじゃただのハッタリとしか思われないよ 541 名前：１３２人目の素数さん [2011/11/27(日) 07:18:09.67 ] suimasenga 圏論と論理学の関係について教えてください 清水によれば圏は普遍論理だそうですが 542 名前：１３２人目の素数さん [2011/11/27(日) 08:31:32.56 ] >>540 ぶっちゃけ、第一より第二が大事！と発狂する奴は 「無矛盾厨」なる人格障害の可能性が大。 >>529の研究の中には、以前、紹介があった自己検証体系も 含まれると思われるが、あれはあれでちょと面白い。 どうでもいいが平方剰余の相互法則のような エレメンタリーな「算数」をありがたがる 小学生は無限を扱うこのスレッドには 立ち入らないでいただきたい。 543 名前：１３２人目の素数さん [2011/11/27(日) 08:37:22.48 ] 論理推論を算術計算でシミュレートする、というアイデアを 数学として認めたくない人はいる。大抵は爺ィだが。 544 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 09:59:03.95 ] >>540 483 にこんなところで訊くなといっているだけ。 545 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 12:40:59.08 ] >>542 平方剰余の相互法則はエレメンタリーな ままでは終わらない、とても深い理論。 代数屋はもちろん、幾何でも解析でも こんなことは常識なのに、基礎論屋とはやっぱり 感覚が違うなと感じる。 常識をわきまえたうえであえて傍流に入ると言うなら まだわかるが、常識を最初から認識してない。 数学で無い別の価値観をもった非数学分野だと いうなら、それでいいんだけど。 546 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 14:03:31.53 ] >>545 自演乙 547 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 15:37:47.45 ] >>545 平方剰余の相互法則は、幾何や解析どころか 代数でも自分の研究とは無関係と思う人は数多い。 これこそ常識であって、545の考えは他の数学者には 通用しない「俺様常識」に過ぎない。 548 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:26:01.98 ] >>547 そんな事はない。 そんな事言ってるのは、せいぜい、数学の流れを見る余裕も無く、 学位や就職の為だけの論文作成作業におわれている 底辺院生か底辺ポスドクぐらいだろ。 549 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:32:04.61 ] >>547 たぶんあなたの言っている数学者は、 かなり広義の意味であって、志の低い人たち。 歴史に名を残す様な数学者は一人もはいっていないと思う。 550 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:33:17.10 ] コイツどんだけ数論を過大評価してるんだｗｗｗ 551 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:39:40.24 ] っていうか、まともな数学者の多くは、 代数とか幾何とか解析とか数論とか、分けてなんかいないよ。 何でも使うから。 552 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:51:54.56 ] んだ。必要ならメタ数学の定理も使う。 553 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 17:04:33.97 ] >>552 少しね。でも、基礎論のアイデアを 使うだけで、基礎論の研究は使わ無い。 というか、基礎論の重要な成果のほとんどは もともと普通の数学者が作った。彼らを後世が どう呼ぶかは後世の人が決めたのであって、 やってる数学者本人は、自分の専門分野なんて 気にしてない。 基礎論からキャリアをはじめて基礎論屋を 名乗っている人のやってる研究はみんな役に立たない。 (一部の役に立てようとして研究しているものは除いて) 554 名前：１３２人目の素数さん [2011/11/27(日) 18:55:45.54 ] 今のロジックの主流はモノイダル論理ですね。 これは∧と∨を同一視したものです。 またリテラルはAと¬Aを同一視します。 これは圏論との関連もあって非常に重要な位置を 数学基礎論において担っていますね。 数論はモノイダル論理で書き換えることができます。 例の平方剰余の相互法則もモノイダル論理の一推論規則にすぎないです。 555 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 19:51:33.51 ] >>554 何の狙いがあって、そんな事をやっているのですか？ 556 名前：１３２人目の素数さん [2011/11/27(日) 19:58:40.23 ] 「すぎない」を使う奴の文章は信用しないことにしている 557 名前：１３２人目の素数さん [2011/11/27(日) 20:23:24.33 ] >>555 まずモノダイル論理はすべての計算モデルで解釈可能です。 次に非常にシンプルでコンパクト閉圏と対応しており、 数学全体の記述をすることも可能です。 おそらくモノダイル論理が導入されたのは ジラールによる線形論理の研究がはじめてでしょうが、 今では言語哲学、分析哲学、計算機科学、公理的集合論といった あらゆる世界で運用されるようになっています。 クミルの竪琴とよばれる推論規則などは 修正クリプキ構造T1-Stepを張ったデントライトの海で 展開される特殊なモノダイル論理で、ジュークの宇宙を再現することができますね。 特にフィッシャーのSSS_ΩやF0-代数との関連で注目されています。 558 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:18:49.35 ] ＞基礎論の重要な成果のほとんどはもともと普通の数学者が作った。 まず、基礎論の重要かつ基本的な成果はゲーデルによって挙げられた。 述語論理の完全性定理、自然数論の不完全性定理、選択公理の相対無矛盾性etc． 「普通の数学者」が基礎論以外の数学でも成果を挙げている、という意味なら ゲーデルが基礎論以外の数学で挙げた重要な成果を一つでいいから教えてほしい。 559 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:20:42.82 ] >>558 ゲーデル解 560 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:22:52.18 ] >>559 残念ながら、その成果は、ゲーデルが論理学においてあげた 華々しい成果に比べると大したことがない。 561 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:26:19.72 ] ゲーデルはロジシャン中のロジシャンだろ 数学者ではない、と思う 562 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:05:06.09 ] ゲーデルは相対性理論もやった 563 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:06:38.16 ] >>557 ですから、そうする事によって、何を目指しているのですか？ 564 名前：１３２人目の素数さん [2011/11/27(日) 22:16:57.58 ] >>563 理論物理や数論幾何で頻出するユニポテント群の 構造解析にマスセル-ドーソンの創造なんていう 解釈可能世界を導入する際にユニ楽園という 議論領域の全体を動くような広義圏論のステンレステンソル代数の 一つのアイディアとなるってことですね。 パースのアイディアは存在の海なんて煩雑なものだから。 565 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:22:34.16 ] 無茶苦茶やなぁ 566 名前：１３２人目の素数さん [2011/11/27(日) 22:24:23.93 ] それからブラウンが提唱した形式の法則なんかはCalculusに基く ブール代数の構成を可能にした「区別」という、 マトゥラーナ＝ヴァレラ図式による拡大可能な システムの自己観察機能による再循環になってる。 例えば「横断」による算法、これは自己同型写像による対象aの分布関数 R：Spec(�農N0)；B(a,ε)→Vll(-<>r) を意味するもので、primary algebra の公理からアイオーンの時間の固体化、 即ちリンデンバウム補数の位相が閉であること(ArrX/R)、 また複素散乱ウカシェベッチ型ベクトルの縮減対応から得られる 「埋め込み」が線型写像であること⇔Θ：ξ(Asc(3))ΛΓ(A_0)→Γ(A_0)の作用が存在する。 直線的被覆が「シミュラークルの質料」というXの規定なんかが有名。 567 名前：１３２人目の素数さん [2011/11/27(日) 22:28:12.64 ] さらにはヒルデガルド対応ってのがる。 一般Tate仮説の∃¬%がKe(C*)の底鎖列として定義される場合に、 任意カントール空間の実効的閉集合世界のMedvedev次数構造が immunityは以下の可換図式と同値。 s → bl → bel → I 　　　　　↓　↓ 　　　　　b → tl → w つまりVintage代数がストーン双対ってこと。 あとは、identification in the limit をベール空間の集合へ一般化した 学習還元可能性。学習は以下のようなもの。 心象自制有界学習(P ≦bl Q)： (∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P & #fn :(g n) , (g n + 1)g < c]: 誤謬有界学習(P ≦bel Q)： (∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P & #f(g n) : n 2 !g < c]: 剰余類学習(P ≦tl Q)： (∃ψ,;;;;,ψ_k )(∀g∈ Q)(∃m ≦ k) limnψm(gn)(g) ∈ P: あるいは、ジュリア閉集合が、 (∀m) P ∧ Im ≠�唐ﾆなるような 有理区間の計算可能な枚挙fImg が存在しないとき。 568 名前：１３２人目の素数さん [2011/11/27(日) 22:29:33.79 ] さらに、中間休止RC0が論理のイマージュとなった「差異」、 セリーの合弁写像Fmin：など、アームストロングの公理系による裏付け、 ドゥルーズのindetermineとideeの分裂など・・・。 最近では以下のようなボニファスの記述(無限還元公理)がある。 Tc1：aを中心とした推論可能域をｒをa；ｒと記述する Tc2：消滅を∃¬%とする Tc3：∃¬%のヒルデガルド対応は∃%である Tc4：∃%の次は0；ｒとする Tc5：0；ｒ→1；ｒの対応でModanponetが一階無効 569 名前：１３２人目の素数さん [2011/11/27(日) 22:30:40.26 ] ちなみにセリーの合弁写像の根拠を与える。 ギヨーム理論が数詞と内部空間をゼロ複数、S単数などの空間的配置で 形態論に内在する意味の精神過程を捉えるエルチュードだとは自明。 P; Q 2 ω＾ω だから、P がQ にculervent還元(P s Q) とは、 ある双対アルゴリズム が存在して，任意のg 2 Q に対して (g) 2 P となるときを指すから、T の定理とL反駁の 分離関数全体の集合Sep(T) はr.e.separating class と呼ばれる特殊な実効埋蔵閉集合になる。 つまり完備側芽のTerr分解X_0[−，]：が以下のように変形される。 Ps j= (8x; y)(9z)(x < y ! x < z < y). (9e0; : : : ; ek )(8g 2 Q)(9m k) em(g) 2 P これがセリーの合弁写像と同型である。 570 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:38:25.64 ] つまらない 571 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:43:35.02 ] 知の欺瞞、ﾁｮｰひもカルト、圏論カルト 572 名前：１３２人目の素数さん [2011/11/27(日) 22:49:54.30 ] 具体的な内容についていけない場合は カルトと批判すればOKとｗ 573 名前：１３２人目の素数さん [2011/11/27(日) 23:21:58.96 ] >>566-569 止めろ。アホ！ 574 名前：１３２人目の素数さん [2011/11/28(月) 00:05:28.92 ] >>572 ｗをつければ高みに立てると思っているのだろうか 575 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 02:29:48.13 ] >554 ついていけなくて悪いが……モノダイル論理ってもしかして双対を扱えるの？ もしそうならちょっと興味があるなぁ。 576 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 03:20:01.88 ] >>575 知の欺瞞 577 名前：１３２人目の素数さん [2011/11/28(月) 10:26:41.08 ] >>566-569 もっと書け！ 578 名前：１３２人目の素数さん [2011/11/28(月) 10:37:03.52 ] 情報板ではダメそうなのでここにきました．教えて下さい． プログラムの表示意味論って何のためにあるのですか？ 分かり切ったことをあらためて書き下しているようで狙いがわかりません． おまけに継続やエラーや入出力などつまらない所（論理の範囲外である 所）で当然のようにツギハギを重ねているようにみえます． そのツギハギが表示的意味論の生き甲斐なのでしょうか？ 579 名前：１３２人目の素数さん [2011/11/28(月) 18:16:29.65 ] 質問です。 不完全性定理を証明するために、形式的体系を算術化しますよね。 その算術化の方法について、どうしてβ関数によるものを考えるのでしょうか。 田中「数学基礎論講義」には 「形式的算術では指数関数が最初から与えられているわけではないので、それとは異なるコード化技法が必要になる」pp.57 とあります。 しかし形式的体系（たとえばPA）に指数関数記号がなくても、 原始再帰関数（つまり指数関数）は表現可能なのだから、実質的には指数関数記号があると考えてもよい気がするのですが。 どうなのでしょうか。 580 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:46:48.46 ] 掛け算がないだけで第一不完全性定理も成立しませんので。 581 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:50:25.58 ] その表現可能性を示すためにβ関数を使うんじゃなかったっけ？ 582 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:58:31.98 ] 東大のゲーデルと20世紀のやつの三巻にそのあたり詳しく書いてある 583 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 19:06:59.11 ] あれは駄本個人的に 584 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 20:34:05.86 ] 理由書かないと駄レス 585 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 21:13:44.36 ] あれは良本個人的に 586 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 22:34:14.39 ] >>578 妙に的確で変な質問だな。自分からは言いたくないもんだから誰かに言わせたいみたいな。 理由自分でちゃんとわかってるだろ。 587 名前：スレタイスレ446 [2011/11/28(月) 23:54:27.03 ] >>578 表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。 大雑把に言って、 表示的意味論≡数学的意味、 操作的意味論≡抽象機械、 公理的意味論≡論理学的意味。 プログラミングの文脈で述べられるが、 見方によっては数学のモデル理論なんかも表示的意味の領域理論の一種と呼べる。 公理的意味論は普通の数理論理学だけあって 決定不能な命題が他の意味論より発生しやすい。 たとえば並列性の概念をもった理論などは、 数理論理学では一般に記述不能。 これは並列性特有の非束縛決定不能性(Unbounded nondeterminism)命題などが原因。 例えばデッドロックみたいなイメージ。 ただし時相論理なんかで計算状況の断片だけ切り取ったりするくらいは可能。 その一方でKowalskiが計算可能性よりも推論規則の方が 多くの命題を生成可能であると証明しているから、 単純に包含関係があるわけでもない。 以前向うのスレで紹介したゲーム論的意味論で不完全性定理が成り立たない自然数論の構成も、 単純な表示的意味論による解釈を2つのプレイヤーの戦略に置き換えると、 並行的な現象であるクラスの決定不能性が破れてしまうという原理によるものだろう。 ちなみにエラー補足や継続などもプログラム言語の内部。 >>579 コードとデコードの保証。算術化って素数の冪乗でもできるけど、 PAに指数関数なかったら例えば論理式なんかがゲーデル数化できない。 >>582 田中の本をまとめたのがその本だよ。 588 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 00:04:16.60 ] >>579 追記：詳しくはその本の9章参照。 589 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 01:30:11.43 ] >>578は何を読んで次の様に感じたのだろうか？ > おまけに継続やエラーや入出力などつまらない所（論理の範囲外である > 所）で当然のようにツギハギを重ねているようにみえます． 表示的意味論でもcontinuation semanticsのスタイルで最初から記述すればツギハギにはならない。 ただ初学者向けにdirect semanticsのスタイルで定式化してからエラーや入出力を扱うとなるとcontinuationスタイルに変える必要がそこで生ずるので 知らない人にはツギハギみたいに見えるかも。 因みにcpoやそれに関する再帰方程式に関する領域論は別にして、トイ言語でないプログラミング言語に対する表示的意味論については 日本語ではロクな教科書はないので、英語の教科書で勉強するしかない。日本語の教科書によっては「表示的意味定義とはインタプリタを書く事である」 なんて大きな勘違いをしているとしか思えないのが岩波の某有名教科書シリーズにあったりするからね。 >>587 > >>578 > 表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。 > 大雑把に言って、 > 表示的意味論≡数学的意味、 > 操作的意味論≡抽象機械、 > 公理的意味論≡論理学的意味。 公理的意味論は、論理的意味というよりも証明の為の形式的体系で、それに対する解釈を与え、公理的意味論の健全性の基準を与えるのが 表示的意味論と考えれば良い。公理的意味論を与えただけでは矛盾していたりする可能性があるが、同一のプログラミング言語に 表示的意味論も与えて、その表示的意味という解釈に対して公理的意味論の体系が健全である事を示せば、公理的意味論で与えた 証明体系を安心して使用できる事になる。 これが>>578が質問していた表示的意味論を与える意義は何か？という問いへの答え。 590 名前：１３２人目の素数さん [2011/11/29(火) 01:34:42.22 ] >>588 その本のpp80の注意.には PAにはすべての原始再帰関数に対する関数記号とそれらに関する公理が入っていると考えてもよい とあるので、原始再帰関数である指数関数の記号と公理もPAには入ってると考えてもよいのですよね？ となると、β関数の意義って何なのかがよく分からなくなるのですが、いかがでしょうか。 591 名前：１３２人目の素数さん [2011/11/29(火) 02:46:09.24 ] representable functor 592 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 07:12:51.67 ] こんなところで訊くなといっているのだが、わからないやつだね。 原始帰納関数が何故、表現可能となるか、とくに帰納法のところを どう書くか考えないで、結果が成り立つことばかりいっているから わからないのだ。 593 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 07:45:34.33 ] >>575 コンパクト論理のことだろう。 >>589 それが正しい回答だろう。 >>590 スコーレム関数として考えると、 理論から関数記号をとっても、 その関数に関係する論理式をユニークにとって保存拡大できるので、 はじめから原始再帰的関数をすべて入れてても結果は同じ。 しかし今回は指数関数が入っていないとして話を始めるので β関数を導入しますよ、ということ。 594 名前：１３２人目の素数さん [2011/11/29(火) 18:25:42.28 ] >>592 周りに聞ける人がいないもので。 今質問しているのは、形式的体系の算術化に関することなので、表現定理云々はあまり関係ないように思うのですが。 >>593 コメントありがとうございます。少し考えをまとめます。 第二不完全性定理を証明する際にPAの証明をPA内部で証明しますよね。 そのとき、形式的体系を指数関数を使ってコーディングするかβ関数を使ってするかで、その方法は異なってきますよね 指数関数によるコーンディングを選んだ場合、PAの証明をPA内部で証明するにはPAに予め 指数関数記号とその公理が予め含まれていないといけないように思われます。 これに対して、β関数によるコーディングを選んだ場合なら、予め指数関数記号とその公理がPAに含まれていなくても、 PAの証明をPA内部で証明することができます。これがβ関数を導入する意義であります。 しかし、>>590,593にあるように実質的にはPAには指数関数記号とその公理が備わっていると考えてもよいので、 実は指数関数でコーディングをしても、PAの証明をPA内部で証明するには何ら不都合はない。　　　　　　　□ 以上の考え方でおかしいところはあるでしょうか？ よろしくお願いします。 595 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 19:08:35.84 ] いや指数関数が入ってない場合は β関数はもっと前に第一不完全性定理を証明するときに 既に導入されるでしょ 596 名前：スレタイスレ446 [2011/11/29(火) 20:50:01.89 ] >>594 そんな感じですね。 カントール対関数でユニークにエンコード、 β関数でユニークにデコード、 両方とも可証性述語の定義に必要。 指数関数というか原始再帰的関数とそれに関する公理を すべてぶっこんだPAの保存拡大はPRAとかよく言われます。 余談：ところで不完全性定理はT|-/-Con(T)でしたが、 Π1^0文に関してはWKL0|-φ⇒PRA|-φとなり、 ヒルベルト・プログラムの断片的実現と呼ばれます。 ですからケーニッヒ補題が超越的とかいう書き込みが上の方にありますが、 ケーニッヒ補題を使った文は有限の立場の文に置き換えれますね。 597 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 20:54:48.16 ] 全くわからないやつだね。 有限列をどうやって表すかってことなんだよ。これができなければ、 なにも表現できないんだよ！ 598 名前：１３２人目の素数さん [2011/11/29(火) 22:07:07.10 ] >>595 β関数を導入しなくても、第一不完全性定理は、 PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できると思うのですが。 >>596 よかった、>>594の考え方であってたのですね。安心しました。 PRAなるものがあるのですね、知りませんでした。勉強になります。余談に関しては知識が追い付かずよく理解できませんが、 いずれ分かるようになれたら良いと思います。 >>597 私の読解力がないせいだとは思うのですが、言っていることがよくわかりません。 「有限列をどうやって表すか」というのは形式的体系を自然数に エンコードする方法のことですよね？いろいろ種類はあると思いますが、 私は素数のべき乗によるものと対関数によるものぐらいしか思いつきません。 599 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:19:13.98 ] 要するに、論理式で書くというkとがわかっていないんだね。 600 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:27:47.20 ] >>596 PRAはPAの保守拡大どころか、それより弱い体系なんだけど…… ＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる 要は E(x,y,n) : y = x^n とか P(x,y) : 「y は x の証明である」とかを 加法と乗法だけを用いた論理式で表現しないといけないわけだけど、 どうやって実行するつもりなんですか？ 601 名前：スレタイスレ446 mailto:sage [2011/11/30(水) 07:48:04.07 ] >>600 ＞PRAはPAの保守拡大どころか、それより弱い体系なんだけど…… 確かにそうでしたね・・・。 量化付きの文の帰納法が制限されていたのを忘れていました。 だから有限の立場というんだった。 602 名前：１３２人目の素数さん [2011/11/30(水) 09:33:43.93 ] >>600 表現定理により、原始再帰的関数および原始再帰的述語はPAにおいて数値別に表現できますよね。 となれば、たとえば8=2^3はPAにおいて、PA|-8=2・2・2・1　と表現できるのではないのでしょうか。 ・・・と思いましたが、なんか怪しいですね。 表現定理は一応一通り自分で証明したつもりだったんですが、改めて各文献に目を通したらきちんと理解してなかったみたいです。 とくに今になって>>592さんの言う原始帰納法の箇所が実はめちゃくちゃ大事だったことに気が付きました。 今日もう一度しっかり勉強してから、質問させていただきます。 ありがとうございました。 603 名前：１３２人目の素数さん [2011/11/30(水) 09:44:15.71 ] 追記： ＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる この発言に関して、完全に私が誤ってました。 604 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 10:10:00.35 ] cs2011_terui.pdfがピンポイントかも。 605 名前：１３２人目の素数さん [2011/11/30(水) 11:36:54.26 ] >>586 >>587 >>589 ありがとうございます．参考になりました． でもやはり表示的意味論の爽快感がどこにあるか不明です． （健全性の根拠というのも内向きの意義のようですし） λ計算の意味論は自明なほどに簡潔です． プログラミング言語と表示的意味論とは本来似合わないのでは？ 表示的，操作的，公理的の３分類もいまいちですね． 意味論といえば表示的に決まっているでしょう？ 公理的意味論はむしろ証明論ですね． 606 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 20:26:05.47 ] >>605 横からスマン、 個人的な意見だけれど、表示されるものがなんなのか明確なコンセンサスが あるわけじゃないからいろんな理論が出てくるんだろうと思っている。 表示されたものがなんであるかによってその３分類が出てくると考えると そこそこしっくりくる。 607 名前：589 mailto:sage [2011/12/01(木) 02:32:26.27 ] >>605 > でもやはり表示的意味論の爽快感がどこにあるか不明です． > （健全性の根拠というのも内向きの意義のようですし） しかし、プログラミング言語に対して定義したホーア論理の体系に対して健全性が保証されていなければ、そのホーア論理の体系で検証しても 全くの徒労となる可能性があるのだから、公理的意味論に対して健全性を示す事は最低限必要不可欠な事ですよ。 > λ計算の意味論は自明なほどに簡潔です． それはλ計算はプログラミング言語として見れば極めて単純なトイ言語だからに過ぎない。 それと、意味定義に用いるメタ言語がλ記法という、対象言語のλ計算とそっくりのを用いるから更に簡潔に見えるだけ。 > プログラミング言語と表示的意味論とは本来似合わないのでは？ プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。 プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。 それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、 表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。 プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。 > 表示的，操作的，公理的の３分類もいまいちですね． > 意味論といえば表示的に決まっているでしょう？ それは数理論理学屋の立場からすればその通りだが、プログラミング言語に対する形式的意味論の研究は、 数理論理学屋がプログラミング言語の研究に流れ込んで来るようになる前の1960年代後半〜1970年代初頭に既に始まっているから、 コンピュータ・サイエンスの歴史からすれば、君のその主張は全く正しくない。 自然言語の意味論にしても、数理論理学の立場からは「意味論」という名前が相応しくないと感じる様々な意味論がある様にね。 > 公理的意味論はむしろ証明論ですね． これも数理論理学の立場からすればその通りだし、589に書いた通り個人的には同じ意見だが、 587の人が書いている通り、プログラムの論理的な側面を「知る」為の「意味論」というのがコンピュータサイエンスの立場。 608 名前：１３２人目の素数さん [2011/12/01(木) 05:54:50.23 ] >プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。 了解です． >プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。 了解です． >それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、 >表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。 それが表示的意味論の具体的なメリットの一つですね． >プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。 そういう意味では，今のプログラミング言語は改める必要があることが既に示唆されているということでしょうか？ 609 名前：１３２人目の素数さん mailto:sage [2011/12/01(木) 08:38:45.01 ] >>605 >λ計算の意味論は自明なほどに簡潔です． 操作的意味論のこと？ λ計算だって表示的意味論、 というかスコット理論がが理論的根拠だよ？ 610 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:27:19.05 ] D無限大モデルが自明とは恐れ入るな。 611 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:28:56.89 ] 天才現る 612 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:40:45.48 ] >>393とか、ちょっとでも理解できていたら、 表示的意味論が無意味とかλ計算の意味論が自明なんて思わないだろう。 613 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 22:25:41.47 ] 写像を学んでて思ったただの感想なんだけど、一般項とか自然数てなんだろうな。数列が 2,4,6,8,10,,n,,と並んでる場合一般項は2＋2(n-1)だ。 しかしこの並びを集合と考えると、この集合はmap(N,N)に含まれる 写像の一つに過ぎない。つまり｛f(1)=2、f(2)=4、、ｎ、、｝という写像。 そう思うとmap(Ｍ、Ｎ）の一般項てなんだろう。んで別に一般項て わけじゃないけど、全単射というのがある。 そうすると自然数というかa<b<c...というように規則を持つ無際限な並びと いうのは、map(Ｍ、Ｎ）に含まれる写像のうちで、ＭからＮへの全単射を持つ 写像という様に考えたほうがいいのかもしれないと思った。まああくまで集合 ありきの考え方であって、自然数は集合から定義されるものではないのかもしれ ないけど。 614 名前：613 mailto:sage [2011/12/02(金) 22:26:55.37 ] 間違えた。｛f(1)=2、f(2)=4、、ｎ、、｝の｛は（だわ。 615 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 01:19:17.26 ] 間違えてるのは書き込むスレッド 616 名前：１３２人目の素数さん [2011/12/03(土) 01:26:34.73 ] 知的財産・受験生ブロガーの一覧 士業名鑑 www.samrai-index.com/04benrishi/benrishi_blogJ.htm 弁理士試験ストリート benrishi-street.com/ 617 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 02:06:54.44 ] >613 余代数ネタ？ ペアノの公理からして後続関数による定義だしな。 618 名前：613 mailto:sage [2011/12/05(月) 13:14:10.95 ] >>617 すまん勉強不足なもんで言ってる事がわからん、、 集合論を学んでると数に対する自明な感覚が失われてきて、もっと上手く定義 しなおせられれば気持ち良いんだが、わからないとものすご気持ち悪いまま終 わると言う感じ。が続く 順序数、とか、同型でない、とかなあ。 自然数は全然自然な無限でもなんでもないという事はよくわかったし、そういう横並びにかつ規則を 持って並んでる無限だけが無限じゃない、という事もわかった。でもそれは濃度と、写像（全単射）の 概念があれば十分なんじゃなかろうか。順序型ωと濃度アレフ０って区別のアプローチが違うだけで どっちかがあればどっちかが要らないような気がする。 619 名前：１３２人目の素数さん [2011/12/05(月) 14:46:58.37 ] >>617 0と後者関数から自然数全体を生成するのは 自由代数の最も基本的な例だから 余代数ではなくて代数。 余代数ならばωから下ってくる形の定義法になる筈。 620 名前：613 mailto:sage [2011/12/05(月) 16:41:32.92 ] ちょっと理解に苦しむまま集合への３０講を読んだ。６１３から感想を 乗せてしまって申し訳ないんですが、最後に１つ質問。 選択公理によって議論が巻き起こったと言う話があるようですが、そもそも 対角線論法は選択公理なしで行えますか？大まかな最低限の段階として １自然数の集合が持つ元から、実数の集合が持つ元をただ一つ指定する。 ２自然数の集合が持つ全ての元から、実数の集合の元をただ一つ指定する。 ３自然数の集合が持つ全ての元から指定された実数の集合の元が、実数の集合 の元全てであるとすると、実数の集合が元として持たない実数が存在する事になり、 矛盾が生ずる。 ４自然数の集合が持つ全ての元の個数（濃度）と、実数の集合が持つ全ての元の 個数（濃度）は異なる。 １の「実数の集合が持つ元をただ一つ指定する」、は選択公理なしで行えますか？ また １の「自然数の集合が持つ元から」、という部分は、つまり自然数の集合が持つ ただ一つの元からという事でしょうか（もし自然数の二つの元から指定していたら、 そのうちの一つによって実数の集合が持たない実数も指定できてしまうから）。 この場合、これは選択公理なしで行えますか？ 621 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 18:30:24.42 ] 自然数と実数に1対1対応できないと言う証明、 >>620 証明を見直してもらうといいが、 選択公理なしに具体的な関数がつくれればいいわけ。 自然数の対角線論法なら選択関数はいらない。 ついでに、 集合とそのべき集合の濃度がちがうことは選択公理なしに証明できる。 （カントールベルンシュタインの定理） 基数にしてもきちんと公理的集合論の教科書のほうがやさしく書いてあるのに。 622 名前：613 mailto:sage [2011/12/05(月) 18:53:32.78 ] >>621 回答ありがとうございます。 ＞具体的な関数がつくれればいい ふむ、、自然数と実数なら単純にf(x)=xと考えられるからと言う事でしょうか？ あんまり多分野の数学を知らないので　（a,b)　←関数によってこの形に（一意に） 出来ない集合同士というのがいまいちピンと来ないのですが、集合にも色々あるん ですね。 ＞きちんと公理的集合論の教科書 教科書選びは難しいですね。。 623 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 19:04:59.68 ] >>620 613もそうなんだけど、ちょっと何言ってるか分かんない あと「集合への30講」はちょっと古い本で、 集合論の入門書として必ずしもいい本ではないので注意した方が良い。 というかそれ以前に数学の文章のまともな書き方を勉強した方が良い。 624 名前：１３２人目の素数さん [2011/12/05(月) 23:23:39.39 ] たびたび質問してすみません。 Boolosの『THE LOGIC OF PROVABILITY』をお持ちの方に質問です。 pp.37のFinSeqという論理式の定義 : ヨa<s ヨb<s ヨk<s (s = pair(pair(a,b),k)) ∧ ∀c<s ∀d<s (pair(c,d)<pair(a,b)→ヨi<k β(c,d,i)≠β(a,b,i)) において、∧以降の定義の意味がよくわかりません。 場合によっては、(pair(c,d)<pair(a,b) かつ ¬ヨi<k β(c,d,i)≠β(a,b,i)) もありうるため、このような定義をしているのでしょうか？ よろしくお願いいたします。 625 名前：１３２人目の素数さん [2011/12/05(月) 23:59:57.03 ] >>624 しょうもないツッコミを入れるが、お前p.とpp.の使い分けの意味わかってないだろ 626 名前：１３２人目の素数さん [2011/12/06(火) 00:09:09.82 ] >>625 わかってません・・・ ちょっとかっこつけて書きたかったんです。 627 名前：１３２人目の素数さん [2011/12/06(火) 00:17:05.39 ] ページをまたがるときは、pp. なんですね。 628 名前：１３２人目の素数さん [2011/12/06(火) 00:24:54.73 ] https://svn.kwarc.info/repos/kwarc/doc/macros/fromCTAN/cv/currvita/currvita.sty 629 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:04:28.35 ] 〜広めてください。 ▼スイス政府 国民保護庁　著「民間防衛」(civil defense) 武力を使わずに他国を侵略する段階を説明しています。 マスコミは乗っ取りがほぼ完了しており機能していません。。クチコミでも身近な人に広めましょう。 日本は今、侵略されつつあります。平和ボケから目覚め、行動を起こしましょう！ 現在第五段階です。 ＴＰＰ ・ 日中韓ＦＴＡ ・ 人権擁護法 ・ 外国人参政権　などが実現してしまえば最終段階が始ってしまいます。 猶予がありません。声を挙げて下さい！ 第一段階「 工作員を送り込み、政府上層部の掌握と洗脳 」 第二段階「 宣伝。メディアの掌握。大衆の扇動。無意識の誘導 」 第三段階「 教育の掌握。国家意識の破壊 」 第四段階「 抵抗意識の破壊。平和や人類愛をプロパガンダとして利用 」 第五段階「 教育やメディアを利用して、自分で考える力を奪う 」 最終段階「 国民が無抵抗で腑抜けになった時、大量移住で侵略完了 」 630 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:11:52.60 ] ↑ 他はともかく、ＴＰＰが何でそこに入っているの？ｗ オマエも何らかの利害関係者じゃん 631 名前：１３２人目の素数さん [2011/12/06(火) 23:30:58.11 ] >>602 ゲーデル数のデコード関数定義にどうしても冪関数が必要になります。 >>605 コーディング上の爽快感と意味論は無関係だと思いますよ。 表示的意味論はドメインに重視した考えですし、 意味関数でユニークに決定するという安定さがあります。 しかしλ計算ならまだそれでいいとしても、 π計算やλμ計算だとか高階χ計算みたいな 逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 一方公理的意味論(ホア論理)はプログラムで検証する意図があったみたいですが...。 >>624 例えば有限列ってのがアルファベットの A,B,C,...Zだとして、(A,0)の対をBなどと考えてみる。 Z＝(((...(A,0)...),21),22)　のように22ステップでZに到達するイメージ。 ここで(a,b)がZより小さい、例えば((...(A,0)...),21)なんかだとすると、 (c,d)がそれより小さい、例えば((...(A,0)...),20)だとする。 このとき、β(x,y,i)でxとyで決まる列のiステップ目のアルファベットがユニークにでる。 β((...(A,0)...),21,0)＝A β((...(A,0)...),20,0)＝A のように、A,B,C,...とやっていける。しかし途中で、 β((...(A,0)...),21,21)＝Y β((...(A,0)...),20,21)＝？ のように存在しないステップが出現するはずですよね...。 632 名前：スレタイスレ446 mailto:sage [2011/12/06(火) 23:33:57.85 ] >>631 補足：ちなみに(A,0)はpair(A,0)の略記なだけなので。 そして実際はβ関数で出てくるのはゲーデル数です。 633 名前：１３２人目の素数さん [2011/12/07(水) 10:27:38.77 ] >>631 >コーディング上の爽快感と意味論は無関係だと思いますよ。 あそこの「爽快感」とは，表示的意味論によってどのような「目からウロコ 感」があるかというような意味でした． >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 その方がやりやすいだけ（あるいは単なる退却）なのではないですか？ むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います． なお「操作的」や「公理的」に「意味論」は似合わないです． （最後の３行は分かりにくいでしょうか？） 634 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 12:19:12.81 ] 操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。 ヒルベルトが幾何学の無矛盾性を算術の無矛盾性に還元したのと同じ手法。 だからモデル理論的手法を使うことが出来る。 こういうものに意味がないと思う人は数学は向いてない。 直感でしか理解したくないのなら数学は必要ない。 635 名前：１３２人目の素数さん [2011/12/07(水) 13:10:46.45 ] >>634 >操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。 機械が出てくる時点で数学（ヒルベルトの手法）からは遠い。 >だからモデル理論的手法を使うことが出来る。 だからって？操作的意味論はそういうものだから、ってこと？ >こういうものに意味がないと思う人は数学は向いてない。 こういうものって？けっこう特定したうえでその意味が不明と言って いるのだが。それに今は「数学」はどうでもよいし。 636 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:31:00.45 ] 抽象機械のことでしょ。 状態遷移マシンとかラムダ式とか。 637 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:37:24.44 ] >>631 ベキ関数無しのコーディングは可能だそうだ 代わりにBussの#関数を使う（Edward Nelsonの本で知った） 638 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 15:24:11.98 ] 元の質問者の読んでる新井さんの本も使ってないんじゃない？ 639 名前：１３２人目の素数さん [2011/12/07(水) 17:57:45.02 ] >>636 ラムダ式まで抽象機械とは言わんだろ 640 名前：１３２人目の素数さん [2011/12/07(水) 19:35:21.68 ] >>637 > Edward Nelsonの本で知った 彼の何というタイトルの本ですか？ Edward Nelsonの本で数理論理学関連と言えばPredicative Arithmeticぐらいしか思い付かないのですが（不勉強なもので、それも読んでいません）。 641 名前：スレタイスレ446 [2011/12/07(水) 21:06:19.80 ] >>633 > >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 > その方がやりやすいだけ（あるいは単なる退却）なのではないですか？ やりやすいということですね。 >>587のUnbounded nondeterminism に関連して、 表示的意味論は並列性などの解釈とするのが困難だという趣旨の定理もあります。 とはいえ、表示的が不可能なわけでないので退却というほどでも。 > むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います． これは詳しくききたいですね。 > なお「操作的」や「公理的」に「意味論」は似合わないです． これはどういったことなのか分かりませんでした。 >>634 モデル論的手法が何かはわかりませんが、 シェラとかのモデル理論が使えるのは表示的意味論の方だと思いますが。 数学は形式的には時間の流れがまったく考慮されない逐次的処理という特徴があって、 計算機とは時間の流れが議論に混入するという理解が一般的だと思っていましたが。 >>635 機械で計算するかは余り関係ないと思いますけどね。 ま、チャーチの提唱次第ですかね。 >>637 全く知りませんでした、書名が知りたいですね。 >>638 exp関数なんかの定義に使われていると思います、計算理論入門の章ですね。 642 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:07:02.49 ] BussのBounded Arithmeticにも. x#y = 2^(|x|・|y|) 643 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:09:01.79 ] ちなみに竹内さんの日本語の書籍にも出てきたはず。 644 名前：スレタイスレ446 [2011/12/07(水) 21:48:57.88 ] 限定算術周辺は盲点だった。 しかし定義上冪と似たような性質が用いられている気もするけど。 実際エンコード方法はいくつもあるんだろうな...。 645 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 22:52:37.72 ] 最低x^log(y)くらいの演算がないとgodel numberingがうまくいかない。 冪相当のものがないとまずいのは40年くらい前から分かってきていた。 Bounded Arith.の人たちはこんな事ばっかり考えてるから。 646 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 05:22:04.87 ] スマッシュ関数の定義可能性を保証する公理は \Omega_1 と呼ばれるが、 I\Delta_0 + \Omega_1 は Robinson's Q で解釈可能（Hajek-Pudlak などを参照）。 つまりこの解釈を通せば、ゲーデル数化は Robinson's Q においても可能、ということ。 647 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 14:12:12.58 ] もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら それでも不完全性定理は証明されるの？ これ、どなたか教えてください。お願いします。もしスレ違いならすいません（´；ω；`) 648 名前：１３２人目の素数さん [2011/12/08(木) 14:50:29.19 ] >>647 おもしろそうな質問だが，これだけでは意味不明と思う． 形式的に答えるなら，少なくとも，不完全性定理の証明には，そういうパラド クスの存在はまったく前提とされていない，ということになるからね． 他の人のコメントも見てみて． 649 名前：647 mailto:sage [2011/12/08(木) 15:06:27.52 ] ありがとうございます。。 ＞もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら やっぱり、ここの部分がしっかり定義されていないというコトですか？ ちょっと調べてきます。。 650 名前：スレタイスレ446 [2011/12/08(木) 20:58:21.54 ] >>646 その考えでいくと他にもいろいろな関数ができそうですね...。 >>647 自己言及のパラドクスは不完全性定理の証明でよく見られますね。 自己言及のパラドクスは定義されているわけでなく、 それに類似した現象を指示する慣用句です。 第1不完全性定理は自己言及パラドクスのようなものとは無縁にも証明可能です。 実は最近、マルチエージェントについて考えていた際に、 不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると 不自然なことに気が付きました...これは哲学的な問題ですが。 651 名前：１３２人目の素数さん [2011/12/08(木) 21:48:07.98 ] >>650 >不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると不自然 これもうすこし聞かせてほしいな。もし可能なら 652 名前：１３２人目の素数さん [2011/12/08(木) 23:06:21.79 ] >>647 648、650が言うのでよいと思うが、647が言いたかったのが 「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である； 後者は前者を厳密に形式化したものに相当する」ということであれば （とてもそうは読めないが）、それはその通りだと思う。 フランセーンがどう言うか知らんが。 653 名前：１３２人目の素数さん [2011/12/08(木) 23:11:41.26 ] クレタ人のパラドックスもベリーのパラドックスも死刑囚のパラドックスも不完全性定理の証明に使えるなら、禿頭のパラドックスも使えないかな。 654 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:21:11.51 ] 確かに嘘つきパラドクスと不完全性定理は確かに似ているけど、 通俗的解説書しか読んだことない人にとっては 類似点よりも相違点を理解する方がずっと大切だと思ってください。 嘘つきパラドクスも不完全性も同じなんだ！ とアナロジーで物事を語る入門者の大半はとんでもないことを言ってます。 655 名前：１３２人目の素数さん [2011/12/08(木) 23:22:46.69 ] >>653 くどいのだが、そうしたなんとかパラドックスが「不完全性定理の証明 に使われている」ということはないよね。 656 名前：647 mailto:sage [2011/12/08(木) 23:23:07.06 ] 答えて下さった方々、ありがとうございます。。 >>652 ＞「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である； ＞後者は前者を厳密に形式化したものに相当する」ということであれば ようするに聞きたかったのは、このとうりです。 もし哲学の現場で「嘘つきのパラドクス」がパラドクスでも何でもない、勘違いだったとなれば、 不完全性定理は、それでも証明されるのか、という事です。 僕も>>650さんの哲学的な問題…という所、聞いてみたいです。。 657 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:30:13.21 ] まあdiagramはほとんど同じ形だけどな。 658 名前：１３２人目の素数さん [2011/12/09(金) 01:01:21.60 ] >>655 フナクイムシがシールド工法の開発に果たした役割くらいはあると思う 659 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 06:37:08.51 ] >>650 例えばタワー関数は出てこない。 I\Delta_0 にタワー関数の定義可能性を加えた体系では Robinson's Q の無矛盾性が証明できてしまうので、 不完全性定理により、その体系を Q で解釈することは出来ない。 冪も出てこないということは Hajek-Pudlak に書いてある。 この方法ではスマッシュ関数の入れ子くらいが限界。 それでもゲーデル数化に充分ってところが味噌。 660 名前：１３２人目の素数さん [2011/12/09(金) 09:18:27.66 ] >>656 不完全性定理は、そんな勘違いがあろうがなかろうが、成立します。 それから、そのような考察をするなら、「パラドックス」という言葉 を極力形式的に定義しておくべきと思います（既知の定義もありますし）。 661 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:37.02 ] ゲーデルが論文で挙げてるのはどっちかというと 嘘つきパラドックスじゃなくてリシャールのパラドックスじゃなかったっけ。 嘘つきパラドックスと不完全性定理にはいくつか大きな違いがあって、 まず前者では命題の真偽そのものについて述べているのに対し、 後者は命題の証明可能性についての話です。 前者を形式化したタルスキーの定理では、 「そのような述語は存在できない」という結論になるのに対し、 後者ではそのような命題があっても矛盾せず、それは証明できない命題となります。 但し存在しても矛盾しないというだけで、実際に 証明可能性述語が存在するかどうかは別問題なので、 不完全性定理を勉強するときはかなり手間をかけて 実際にそのような述語を作ることになります。 662 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:58.22 ] 次に嘘つきパラドックスは直接に自分自身の真偽について言及していますが、 不完全性定理で出てくる文章は、直接的には 自然数を足したり掛けたりしたら等しくなるというような命題です。 それが結果的に自分自身が証明できないということと同値になります。 最後に、哲学で出て来るこの種のパラドックスでは 「この文は」というような意味のはっきりしない指示語などが使われているので、 数学者に言わせれば、 日常言語のような曖昧な言葉を使うのが悪いんだよ、ということになります。 不完全性定理では上で見たように自然数の足し算掛け算について 述べているだけの命題なのでそういうことはありません。 663 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:30:39.29 ] いやいや哲学方面も厳密な議論してるよ。 Strong Lier Paradoxってのが、 カントールの定理やTuringマシンの停止問題と同型。 圏論の図式レベルまで単純化すると第一不完全性定理も同型。 664 名前：１３２人目の素数さん [2011/12/09(金) 23:41:57.72 ] おまいら頭悪いなｗ kamome.2ch.net/test/read.cgi/psycho/1284396792/364-370 665 名前：１３２人目の素数さん [2011/12/10(土) 02:54:55.58 ] いまだに第二不完全性定理の証明に必要な導出性条件の証明ができない。 ここの住人はどうやって理解したんだろうか。 666 名前：１３２人目の素数さん mailto:sage [2011/12/10(土) 08:44:44.06 ] 論文読め 667 名前：スレタイスレ446 [2011/12/10(土) 09:38:44.80 ] >>651>>656 不自然な点とは第2不完全性定理なんですが、 大雑把にいえば、モデルを持つ理論が、自らのモデルについては言及できないという言明について、 その条件がモデルを持つことであるために、自己言及できていないのでは？という趣旨です。 当初は単一の世界での不完全性定理を考えていて気が付かないかったのですが、 複数の世界でエージェントの信念や知識を考慮すると不自然なんです。 自己言及のパラドクス的なモノをまだ知らない状況、というものが考えられるなど...。 この考えはまだまとまっていませんが。 >>659 どうも、無料なうえに良書ですね。 >>661 それらをまとめると、タルスキの定理は、 すべての論理式φで、N|=φ←→R(【φ】)なので、 ⇔すべての論理式φで、PA∪{φ←→R(【φ】)}|-φ←→R(【φ】) だからゲーデル文ψでPA∪{ψ←→R(【ψ】)}|-ψ←→¬R(【ψ】)となり、 真偽判定は第1不完全性定理の証明判定の別モードと解釈もできますよね。 つまりそれぞれ自己言及パラドクス（ゲーデル文）が源泉。 ま、実は第1は自己言及も可証性述語も一切必要なしに証明できるんですが。 >>663 同型とは何でしょうか。 668 名前：１３２人目の素数さん [2011/12/10(土) 10:46:36.38 ] >>667 >不自然な点とは第2不完全性定理なんですが、 ここのパラグラフまだよくわからないのですが，なんとなくおもしろそうですね． まとまったら解説をよろしく． 以下は私の中での不明点．もちろんコメントいただく必要はありません． >理論が、自らのモデルについては言及できない 直感的には，これは理論の宿命ではないのだろうか？ >その条件がモデルを持つことであるために、自己言及できていないのでは？ これを文字通りに解釈すると｢その理論が無矛盾であるために自己言及できて いない｣という意味になるが，それはナンセンスではないか だが，こう考えることがそもそも「単一の世界」に捉われているということなのか？ 669 名前：１３２人目の素数さん [2011/12/10(土) 10:50:28.68 ] 世界とかエージェントとかは様相論理の話だと思われる 670 名前：１３２人目の素数さん [2011/12/10(土) 12:14:47.43 ] >>669 それはそうなのだが 671 名前：スレタイスレ446 [2011/12/10(土) 17:08:19.79 ] >>667 訂正： タルスキの定理は正確には、 すべての論理式φで、N|=φ←→R(【φ】)となる述語Rが存在しない。ですね。 >>668 基本的には理論自体のモデルと、その理論から証明される言明中の支持するモデルが同一かどうか考えていますね。 あくまで哲学的な意味でですが。 672 名前：１３２人目の素数さん [2011/12/10(土) 18:43:34.43 ] >>671 ここでいう「モデル」って、たとえば完全性（無矛盾<->モデルの存在） などの文脈で使われる「モデル」と思っていいのですよね？（それとも別の意味？） 673 名前：スレタイスレ446 mailto:sage [2011/12/10(土) 23:33:12.77 ] そのモデルです。 674 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:29:22.34 ] ツォルンの補題を用いて 「Aが無矛盾→Aはモデルを持つ」の証明を教えてください お願いします 675 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:36:12.67 ] 教科書嫁 676 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:40:42.60 ] 教科書ないんです 調べてやれって言われました・・・ 677 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:46:50.90 ] 図書館池 678 名前：１３２人目の素数さん [2011/12/11(日) 23:50:48.14 ] フランセーンが「ＰＡの超準モデルの存在は不完全性とまったく無関係」と 書いているのだが、これはちょっと言い過ぎでないかい？ 679 名前：１３２人目の素数さん [2011/12/12(月) 04:18:24.46 ] 「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可 能である」 これはjに関する数学的帰納法で証明できる。 とあるのですが、どうしてjだけでよくて、iやkについては考慮しないで良いのでしょうか？ 1変数の述語に関しての数学的帰納法はよく分かるのですが、複数変数の述語に関しての 数学的帰納法がよく分かりません。 初歩的な質問ですみません。 680 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 04:53:38.89 ] >>679 jについて、任意の自然数iに対して或る自然数kが存在してi+j=k を仮定し、自然数iを任意に固定して1を右から足すだけ。 あとはiを動かして終わり。 681 名前：１３２人目の素数さん [2011/12/12(月) 06:03:53.48 ] jに関する数学的帰納法で証明できるというだけで、iやkを考慮しなくていいなんて書いてないだろ？ やりたければiやkに関する帰納法でも出来るんじゃない？どういう公理を採用しているのか知らないけど。 682 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:40:24.97 ] >>681 任意の自然数i、jについて、i、jを固定したならペアノの公理からi+j=kも自然数であることが示せるから、jやkは考えなくてよい訳で 「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可能である」 の「任意の自然数 i,j について、i+j=k」は「任意の自然数 i,j に対してある自然数が存在してi+j=k」と解釈した訳だが。 >>679の文についてこの解釈が間違っているのか？ 683 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:42:49.32 ] 間違ってる 684 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:53:51.33 ] >>683 >>679の文章をどう解釈すればよかったのか分からない。 685 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:00:32.23 ] 「任意の自然数 i,j,k について、i+j=k のとき、PAで ”i+j=k” が証明可能である」の間違いだろ。 もしくは「任意の自然数 i,j について、自然数 k が存在して、PAで ”i+j=k” が証明可能である」でも同じことだが。 i,j に対して i+j=k となる k が存在することは小学生でも知っている自明な話。 686 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:49:04.82 ] >>685 i+j=kを満たす任意の自然数i、jについて、PAで ”i+j=k” が証明可能である を示すのか。 ペアノの公理を公理として認める限り、これはトートロジーだろう。 687 名前：１３２人目の素数さん [2011/12/12(月) 10:45:55.80 ] 「任意の自然数 ,j について、1+j=k のとき、PAで ”1+j=k” が証明可 能である」 「任意の自然数 ,j について、2+j=k のとき、PAで ”2+j=k” が証明可 能である」 「任意の自然数 j について、3+j=k のとき、PAで ”3+j=k” が証明可 能である」 … この無限個の命題を数学的帰納法で証明できる、ということでしょ 688 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 11:16:16.25 ] i+0=kに帰結させて、次はi=kであることを示す。 これには数学的帰納法は必要ない。ただし、 S(i')=S(k')と帰納的に0=0に帰結させる。 jを選ぶかどうかは証明したい人の勝手。 689 名前：検便のナウシカ ◆UVkh7uHFoI [2011/12/12(月) 19:21:09.48 ] てｓｔ 690 名前：スレタイスレ446 [2011/12/13(火) 00:37:14.98 ] >>674 それは完全性定理。 ツォルン使うところだけ言うと、 無矛盾な文の集合の族に、包含関係で順序を入れる。 任意に整列した部分集合をとれば有界になってるから、 この族は極大元をもつ。 こいつにAと共に無矛盾性を保つ文がすべて入ってるから、 こいつの解釈を定義すると...。 >>678 どういった文脈でしょうか...。 >>679 仮定の方のi+j=kは、経験的な意味での足し算。 ＞PAで ”i+j=k” が証明可能である こっちはS(S(...S(0)...))のような形をしているが、 i,j,kは数項と呼ばれるメタ変数による略記だと思う。 普通はiかjの片方を任意固定して帰納法を使う。 片方固定しているから、もう片方の選び方で ユニークにkが決まるということがi+j=k という仮定から出る。 この帰納法が第二不完全性定理がPA以上であることとつながる。 691 名前：624 [2011/12/13(火) 02:26:39.96 ] >>631 レス遅くなりましたが、解説ありがとうございます。おかげで疑問点は解消できました。 もう1つ質問させて下さい。（何度もすみません） このスレでも何度か書いていますが、私はどうしてもLoebの可導性条件、特に D3　PA|- Pr([A])→Pr([Pr([A])]) の証明が理解できません。 以下、私がどこまで理解しているかを簡単に書きます。 D3を証明するためには、任意のΣ1文Fに対して、 PA|- F→Pr([F]) が証明できればよく、そのためにはFの構成に関する帰納法で証明すればよいわけですよね。 つまり、以下の１から４の順番で証明すればよいと。 １、F ⇔ x=y, 0=x, Sx=y, x+y=z, x・y=z　のとき、PA|- F→Pr([F]) ２、F ⇔ G∧Hのとき、PA|- F→Pr([F]) ３、F ⇔ ∃xG(x)のとき、PA|- F→Pr([F]) ４、F ⇔ ∀x<y G(x)のとき、PA|- F→Pr([F]) 以上の１以降が理解できなく困っています。たとえば、 PA|- x+y=z→Pr([x+y→z]) はどのようにして証明すればよいのでしょうか。 文献[1]には、これの証明が載っているのですが私にはよく理解できませんでした。 使用している文献は [1]　Boolos「THE LOGIC OF PROVABILITY」 [2]　田中他「数学基礎論講義」 の2冊です。 長くなりましたが、どうぞよろしくお願いします。 692 名前：624 [2011/12/13(火) 02:31:02.51 ] 追記 文献[2]には、D3の証明は膨大な量になるので、これを書き下すのは実際にはかなり困難な作業とあります。 一方、文献[1]には（多少の省略はあるものの）D3の証明を最後まで書いているように思われます。 やはり私がしっかり読めていないだけで、文献[1]も大幅に証明を省略しているのでしょうか？ 693 名前：624 [2011/12/13(火) 02:34:07.71 ] >>691の PA|- x+y=z→Pr([x+y→z]) は PA|- x+y=z→Pr([x+y=z]) の間違いです。失礼しました。 694 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 03:14:10.12 ] >>690 ＞この帰納法が第二不完全性定理がPA以上であることとつながる。 少し前で、第二不完全性定理はPAより遥かに弱い体系でも成り立つ、って話が出ているのにもかかわらずこの発言ｗ 695 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:15:56.94 ] >>691 当り前だが、２は帰納法の条件が抜けている。693 では x+y=z から y=0 の場合、z=x そうでない場合 x+(y-1) = z-1 が導かれる といったことに気づくことが必要。 696 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:21:31.04 ] >>646 で述べられているやり方により、 冪もスマッシュ関数もないロビンソンのQでも第二不完全性定理は成り立つ。 しかし積は必要で、積もないプレスバーガー算術では第二不完全性定理が成り立たないのは有名な話。 697 名前：スレタイスレ446 [2011/12/13(火) 08:13:28.50 ] >>694>>696 例の文脈で言ってたのはゲーデル数化ですよね。 ところでQでは零元との加算の交換法則さえ成り立たないですよね。 PAよりもQの方がはるかに証明可能な論理式が少ないと予想できます。 ところで第一の証明の際に結構数学的帰納法を多用しますよね？ その証明を形式化した第二の可証性述語を証明するのに、 帰納法の公理が一切不要であるということは証明されているのでしょうか？ プレスバーガーにも帰納法は入ってますし。 それとも別の方法があるということでしょうか？ 698 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 17:01:02.16 ] >>697 帰納法もゲーデル数化も扱いは同じだよ。 Qは直接は帰納法を持っていないけど、>>646でいうように 「解釈された帰納法」は持っているので、それで充分。 699 名前：１３２人目の素数さん [2011/12/14(水) 00:18:55.11 ] >>647>>650>>651>>656>>667 不完全性定理と自己言及のパラドクスはかなり異なる。 まず第一不完全性定理の証明にゲーデル文などは必須ではないことに注意。 1階述語論理の充足不能判定性問題の決定不可能性が容易に証明可能だが、 このときロビンソン算術の不完全性は、 後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。 3つを∧でつなげて存在例化したのをAとする。 するとAの任意モデルは標準モデルと同型になる。 さらに文φをある一項述語に相対化してすべての関数述語定数を存在例化したものをφ*とすると、 φ*は一項述語をドメインとするモデルであるかに依存して真偽が決定する。 このテクニックで任意のφについて、 φが決定不能⇔”Aが真ならばφ*が真である”ことが決定不能。 として第一不完全性定理が成り立つ。 また第二不完全性定理については、自らの無矛盾性証明ができないだが、 T|-⊥→φなので、T|-Pr(⊥)→Pr(φ)とT|-/-¬Pr(⊥)からT|-/-¬Pr(φ)がでて、 そもそも任意の論理式が証明できないことが証明できない、 第二不完全性定理はこれの系と言える。 さらにこれらが解を持たないある種の不定方程式と同値であることと、 ほとんどの次数と変数の不定方程式が決定不能なことを考えると、 真でありながら証明可能な論理式は、ほんのわずかしかない。 700 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:05:35.73 ] >後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。 >3つを∧でつなげて存在例化したのをAとする。 >するとAの任意モデルは標準モデルと同型になる。 ほほぅ、それは世紀の大発見ですな。 701 名前：１３２人目の素数さん [2011/12/14(水) 04:33:52.08 ] 集合論は完成された学問ですか？ まだ進化し続けているのでしょうか？ 日本人で集合論を専門にしている方はいますか？ 702 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:57:56.30 ] Mitchellのアーベル圏充満埋め込み定理の読みやすい証明の有る本教えれ。 703 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 05:26:12.73 ] >>701 一般人が「集合論」という名称から想像する学問内容と、 研究現場で「集合論」と呼ばれる研究内容は必ずしも一致しないことも多い。 どのような研究内容を想像しているのか？ 704 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 06:44:06.79 ] スレタイスレ446君は偉そうなこと言う割に、不完全性定理っていう基本的な事実については余りに無知なんだね。 不完全性定理の為の条件である「ある程度の算術を含み、かくかくしかじかの性質を満たす公理系」の内、 「かくかくしかじか」の部分は得意気に解説しているブログはよく目にするが、 最初の「ある程度の算術を含み」がどういうことなのか理解が浅い連中が多い。 PAほど強い必要は全然ないし、それよりも「含む」という部分が曲者。 狭い意味で考えてしまうと、ZFC 集合論と算術は言語が違うのだから算術を含んでいないことになってしまい、 ZFC 集合論には不完全性定理が適用できないことになってしまう。 705 名前：１３２人目の素数さん [2011/12/14(水) 08:06:23.57 ] >>700 前者の存在性に関する公理から任意の論理式φについて、 φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x) の形の文が出現、これを2階述語論理で量化した ∀φ(φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x)) と「後続者関数の単射性」と「0の非後続者性」は範疇的で 何れもω_0のドメインを持つ。このことから、 ”1階の文φ”が決定不能⇔”2階の文Aが真ならばφ*が真である”が決定不能。 706 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 12:41:59.00 ] >>705 2階述語論理で量化...? 707 名前：スレタイスレ446 [2011/12/14(水) 18:53:08.34 ] >>704 >>690でPA以上といったことについてならば、 私は>>679のレスポンスを見て、第一不完全性定理の証明を形式化して 第二不完全性定理を証明しようとしていると予想したんですね。 だから第一の条件がQになるのに対し第二がPAになっている理由を述べたわけです。 PAよりも単純な体系でも証明できるのでしょうが、 例の限定算術についてはほとんど知らないので、 数学的帰納法位は必要なんじゃないだろうか、と考えた末のレスポンスが>>697なわけです。 708 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 20:23:27.08 ] ただ、普通の数学者にとってみれば、 Peano算術をどれだけ弱く出来るかとかそういうことは 専門家のみが興味を持つどうでもいいことなので、 だからこそ指数関数を最初から加えて証明を簡略化したりする 709 名前：１３２人目の素数さん [2011/12/14(水) 20:52:04.65 ] さらに言えば、 再帰的クラスの決定問題については、 去年、Rendellによって構築されたライフゲームの万能チューリング機械により、 ttp://uncomp.uwe.ac.uk/CAAA2011/Program_files/764-772.pdf すべてエデンの園に帰着できることが証明されているので、 ttp://arxiv.org/PS_cache/arxiv/pdf/0709/0709.4280v1.pdf これからは不完全性定理含め、Σ_1・Π_1階層の決定問題はすべて セルオートマトン上で実行されながら研究が進む流れとなるだろう。 710 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 21:48:34.40 ] >>706 正確にはあらゆる論理式に対して 述語定数を定義してから、その述語を量化する。 711 名前：１３２人目の素数さん [2011/12/16(金) 07:26:41.52 ] >>702 Peter Freyd 著 abelian categories 712 名前：１３２人目の素数さん [2011/12/17(土) 01:52:21.32 ] 記号論理学ってここに入りますか？

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef