数学基礎論・数理論理学のスレッド　その7

1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その6 kamome.2ch.net/test/read.cgi/math/1265884076/ 109 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 23:09:36 ] ストーンの定理、ブール主イデアル、完全性定理が同値でなかったっけ。 110 名前：１３２人目の素数さん [2011/01/05(水) 13:01:24 ] ヒューズの様相論理入門』に ●が定理であるなら□●が定理　必然性規則 ●→□●　公理（ここで、●は定理）　は駄目 というくだりがあったと思うんですが 反例が思い浮かばずに（思い出せずに、今、手元に本ありません）苦しんでます なんで駄目なんでしたっけ？ 111 名前：１３２人目の素数さん mailto:sage [2011/01/05(水) 20:19:48 ] 偶然に真だけど必然的に正しい訳じゃないみたいな例を挙げれば良いんじゃないの？ 112 名前：１３２人目の素数さん mailto:sage [2011/01/05(水) 21:24:26 ] A→∀xA　がダメなのと同様に考えればいいんじゃないの？ 113 名前：１３２人目の素数さん mailto:sage [2011/01/05(水) 21:39:33 ] >>108-109 了解しました。というか何となくすっきりしました。 まあACがない場合どうなるか、という仮定だと面白い結果が無いんでしょうね。 wikipediaでは「一階述語論理における意味論的真理と統語論的立証性の対応を確立した」とか いかにも絶対に成立する結果のように書いてるけどｗ 114 名前：１３２人目の素数さん mailto:sage [2011/01/05(水) 22:49:52 ] そりゃあ普通、選択公理は認めるものですし… 115 名前：１３２人目の素数さん mailto:sage [2011/01/06(木) 20:31:31 ] 田中尚夫の公理的集合論 どこにも売ってねえ（ノД｀）゜。゜。 116 名前：１３２人目の素数さん mailto:sage [2011/01/06(木) 20:55:06 ] もう絶版でしょ 古本で買うしかないけど、今はKunenの訳書あるからなあ 117 名前：１３２人目の素数さん [2011/01/07(金) 17:00:07 ] 質問です。アレフって極限基数なんですか?　それとも直前の基数が存在するんですか? 証明付きでおながいします。 118 名前：１３２人目の素数さん mailto:sage [2011/01/07(金) 17:27:52 ] Introduction to Cardinal Arithmetic でgoogleブック検索せよ 119 名前：１３２人目の素数さん mailto:sage [2011/01/07(金) 20:28:07 ] なぜにその本 120 名前：１３２人目の素数さん [2011/01/08(土) 18:15:24 ] 集合論はPDFがネット上にたくさん転がってるでしょ。 121 名前：猫は作業 ◇MuKUnGPXAY [2011/01/08(土) 18:42:30 ] もうエエかァ？　ほしたらや： ■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ■■■■■■■ このスレは他板・他スレ運営妨害の非常に悪質糞スレの為に ■■■■■■ ■■■■■■■反感を買って終了しました。 皆様のご愛顧有難う御座いました■■■■■■ ■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ 猫 122 名前：117 mailto:sage [2011/01/09(日) 21:30:03 ] >>117 答えは解っているのですか？それとも未解決なんですか？ 123 名前：１３２人目の素数さん mailto:sage [2011/01/10(月) 00:35:54 ] どっちも（ZFCから）示せないはず。 2^(aleph 0) が後続基数 aleph(n+1) だと仮定しても 矛盾しないことは昔から分かってる。 （n=0のときGo¨del、nが正の整数のときCohen） 極限基数でも良いんだけど、ただしaleph_ω とかaleph_ω^2とかと 等しくなることは出来ない、というのは簡単に証明できて、 よく一、二年の集合論の期末試験で証明問題として出されたりする。 じゃあどういう極限基数 κ なら良いんだということになると、 少なくとも共終数cf(κ)がωよりも大きくないといけないことは 同様に証明できるんだけど確かこのようなκの存在は証明不可能だったと思う。 つまり敢えて難しく言うと 「「連続体濃度が後続基数であることは証明できない」ということは証明できない」 ということが証明できるということです。 そうは言っても皆「連続体濃度が後続基数であることは証明できない」のは ほとんど確実だと思ってるんですけどね。 124 名前：１３２人目の素数さん mailto:sage [2011/01/10(月) 00:37:45 ] 最後らへん本当にそうなのか不安になって来た。 もっと詳しい人フォローお願いします。 125 名前：１３２人目の素数さん [2011/01/10(月) 07:27:12 ] すみません。どこで質問していいのか判らないのでここかもと思って書いてみました。 親切な方がいたら教えてくれたら嬉しいです。 また、もし「スレチだ、ここに書くな」という人がいましたら、出て行きますが もしできたら適切なスレを教えて貰えたりすると嬉しいです。 では、質問です。 この問題に詳しい人はこんな質問をすること事態が疑問かもしれませんが お願いします。 テレビのドラマを見ていて４色定理というものをみました。 ja.wikipedia.org/wiki/%E5%9B%9B%E8%89%B2%E5%AE%9A%E7%90%86 これなのですが、以下のような地図の時はどうするのだろうか？ということです。 ------------------------------------------- │ 土地A │ -------------------------------------------- │土地B　│土地C　│土地D　　│　土地E　│ -------------------------------------------- こんな形なのですが・・・・ 土地B・C・D・Eは飛び地ということなのでしょうか？ 宜しくお願いします。 126 名前：１３２人目の素数さん [2011/01/10(月) 07:28:31 ] あっ、ごめんなさい。 ------------------------------------------- │ 　　　　　　　　土地A 　　　　　　　　│ -------------------------------------------- │土地B　│土地C　│土地D　　│　土地E　│ -------------------------------------------- こうです。 127 名前：１３２人目の素数さん [2011/01/10(月) 07:32:03 ] 宮崎の口蹄疫、実は韓国産 韓国の口蹄疫ウイルス、宮崎とほぼ一致　水際対策を強化 ttp://www.asahi.com/national/update/0107/TKY201101070483.html 　農林水産省は７日、韓国で大流行している家畜伝染病・口蹄疫（こうていえき）のウイルスを分析した結果、昨年に宮崎県で広がったものと遺伝子配列がほぼ一致したと発表した。農水省は国内への侵入を防ごうと、 空港や港など水際での防疫対策を強めている。 　農水省によると、韓国では昨年１１月に東部の慶尚北道・安東で確認されたのを皮切りに、５道１市とほぼ全土に拡大した。今月７日までに９９例が発生し、牛や豚約１０７万頭が殺処分の対象になった。このほか 約１２０万頭にワクチンを接種中だ。 　このウイルスを韓国政府が分析した結果、宮崎のウイルスと遺伝子配列が９９％以上一致したという。韓国では昨年４月にも発生していた。 128 名前：１３２人目の素数さん mailto:sage [2011/01/10(月) 07:56:01 ] ------------------------------------------- │ 　　　　　　　　土地A 赤　　　　　　　　　　　　　　　　│ -------------------------------------------- │土地B 青│土地C 黄　│土地D 青│　土地E 黄│ -------------------------------------------- でこの場合は３色でOK 129 名前：１３２人目の素数さん mailto:sage [2011/01/10(月) 08:45:46 ] BCK論理ではラッセルのパラドクスが発生しない。 BCK論理を中心とする部分構造論理は数学のすべてを記述するだろう。 130 名前：１３２人目の素数さん [2011/01/10(月) 16:13:01 ] >>128 あっ、そうか。 俺、あほだな。 ありがとね。 131 名前：１３２人目の素数さん mailto:sage [2011/01/13(木) 00:32:45 ] 自然数の0のことを 0: = Ø = { } と定義しちゃったら 空集合と0を区別して使いたい場合に困るじゃないか、 仮に0を退避させてもその先で用途が今後被るかも知れないじゃないか、 っていうことは公理的集合論を勉強し始めたときに気持ち悪い点の一つだと思う。 順序対の定義とかもそうだけど、最初に集合論を勉強し始めたら 結構な人が違和感を持つんじゃないだろうか。 これは、これこれの対象と関数と述語が存在して 自然数論の公理を満たす構造になっている、 という公理系 T を別に考えて理論の合併 ZFC ∪ T を考えれば良くて、 ZFC ∪ T では0=Øみたいな式が証明されることは絶対無いので 実際に数論とかの数学をやるときはこっちのほうが自然。 でも集合論の公理系のことを主に考えている場合は T の∃z 〜〜 とかは実はZFCの公理から普通に証明できるので、 敢えて公理にする必要無いよねって話だと思うと良い。 人間が読めば文脈で区別できます、みたいな返答はあんまりじゃないかなあ。 そりゃそうだがそんなこと言ってるんじゃないだろうよ。 132 名前：１３２人目の素数さん mailto:sage [2011/01/13(木) 06:20:19 ] >>131 ツイッターから出てくるなよゴミカス 133 名前：１３２人目の素数さん mailto:sage [2011/01/14(金) 22:30:41 ] 「数学のロジックと集合論」によると 完全性定理は選択公理よりもちょっと弱いらしいよ こないだ立ち読みしてたら書いてあった 134 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 01:41:29 ] ゲンツェンによる自然数論の無矛盾性証明における 証明図の簡略化は有限回で終わるのか。 言い換えれば、対応する順序数は整礎なのか。 正しいような正しくないような…モヤモヤする… 135 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 06:04:33 ] 最近、数学するときに不完全性定理のことを もっと真剣に考えないといけないと思うようになりました 真とも偽とも判断が付かない命題があるなら 真か偽かを考えると同時に証明できない可能性も考えるべきだと思います そこで、ある命題が「真とも偽とも証明できない」ことを 証明するような手段を知りたいのですが、 何か手順・プログラムなどがあったら教えてください 136 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 08:31:57 ] 簡単なところでは反例を作るとか。 集合論的な独立命題なら強制法使って独立性示したり 他の良く分かっている命題に帰着させたりとか。 137 名前：135 mailto:sage [2011/01/15(土) 18:53:51 ] レスサンクスです 強制法とか参考になります 自分はそれほど論理学をマスターしていないので もう少し詳しく教えていただけるとありがたいです > 反例を作るとか。 これはどのような反例を作ればよいのでしょう？ 真または偽と証明できたと仮定して反例を導くのでしょうか？ しかし不完全性の例だと、真であっても偽であっても 矛盾しないような気がします。 > 集合論的な独立命題なら強制法使って独立性示したり 強制法をいまチラ見しただけでまだよく分かってないのですが 任意の命題（集合論的な独立命題でないもの）に対しては 適用できない手法ですか？ よろしくお願いいたします 138 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 19:58:30 ] 例えば、〜〜という前提のもとでAとnot Aのどちらが正しいのか？ とか言った場合にAを満たす例とnot Aの例の両方を作るとか。 強制法が適用できないような独立命題もあって良さそうなものだけど、 現実問題としてはあまりそういうものは知られてないんじゃないかと思う。 だから独立性のことが気になるなら強制法が一番強力な武器なのは間違いないと思う。 ロジックでは強制法が使えないほど弱い理論（たとえば限定算術）から或る定理が 独立かどうかとかが問題になることもあるのだけど、 普通の数学ではZFCから証明出来たら、証明できたものと見做す。 だいたいAもnot Aも証明できないというのが真実だとしても、 「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。 139 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 20:31:18 ] ありがとうございます！大変参考になります。 > だいたいAもnot Aも証明できないというのが真実だとしても、 > 「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。 そうですね。証明可能性を分類していくと A (が証明できる） not A (が証明できる） 「A か not A か証明できない」（ことが証明できる） 『「A か not A か証明できない」ことが証明できない』（ことが証明できる） と続けて n 段階目を 「A か not A かという」 [ことが証明できない]^n (ことが証明できる） と書ける。これを n 段階証明不可と呼ぶと、 n はいくらでも続けることができてω段階証明不可という命題を妄想します。 さらにω段階証明不可が証明不可であることを（ω+1）段階証明不可として 、nω段階、ω^n段階、ω^ω段階のようなことを妄想します。 これらの可能性を包括的に走査するプログラムなどを当方は妄想していますが 不完全性からは無謀な試みでしょうか？ 140 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 21:46:21 ] そんなつまみ食いで何かできるとしたらよほどの天才 141 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 21:53:19 ] しっかり栄養をつけて食べるにはどう学習したらよいでしょう？ いまのところ戸田先生の『論理学をつくる』をざっと眺めました。 他の論理学の本は、なんだか頭に入ってこないというか、 書き方が難しいです。哲学よりの本も多いし… 数理論理学をやるのによい中級の本はないでしょうか？ 142 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 21:55:34 ] 全く無謀な試みです。 ……なぜかと言うと、矛盾からは任意の命題が出て来るので、 　Tから証明できない或る命題が存在する⇔Tが無矛盾 よって、たとえばZFCで考えているとして、ZFCが無矛盾であることが証明できない限り 三段目以降は全部自動的に無理になってしまう。 これも前のスレにあった話だけど。 やっぱ皆考えることは同じだよね。 143 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 22:02:29 ] >>141 自分は『論理学をつくる』の次に 前原昭二『数学基礎論入門』を読みました。 論理計算を実践しつつ（かなり丁寧）、不完全性定理の厳密な証明が学べます。 命題論理の公理系から始まるので、シンタクスとセマンティクスの区別さえできていれば、 他に予備知識は不要な本です。 144 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 22:32:41 ] >>141 たぶんその栄養が身になるころにはなんのために論理学を身に着けようとしたのか もう忘れてしまっているのに十分な時間が経過していることでしょう。 三途の川の向こうに答えがあるかもしれませんね。 145 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 22:48:53 ] >>142 そうですか… しかしZFCからは連続体仮説が証明できない、という結果があったと思いますが これはZFCが無矛盾であることを示したことにならないでしょうか？ もっと込み入った事情がありますか？ 146 名前：１３２人目の素数さん mailto:sage [2011/01/15(土) 22:51:39 ] >>143 ありがとうございます その本も手元に持っていたので読み込んでみます >>144 まあ数学やる以上は答えが出るか分からない旅… 147 名前：１３２人目の素数さん mailto:sage [2011/01/16(日) 00:43:48 ] >>145 > これはZFCが無矛盾であることを示したことにならないでしょうか？ そうするとZFCは無矛盾でないことになりますので、大発見だと思います。 148 名前：１３２人目の素数さん mailto:sage [2011/01/16(日) 10:30:53 ] >>145 単純に、ZFCが無矛盾だとすれば、の前提つきでの話。 もちろん、矛盾していても証明できるけど。 149 名前：139 mailto:sage [2011/01/16(日) 18:36:25 ] >>147 >>148 なるほど。 よく言われる「連続体仮説は証明も反証もできない命題である」 ということの証明には前提条件があったのですね。 しかしZFCが矛盾するとすると集合論が崩壊するので 数学は致命的なダメージを受けますね。 数学という船にのっている以上、ZFCは無矛盾、と仮定するのは 自然な成り行きだと思います。 言い方は悪いですが、沈むときは一緒だ、みないな。 そこでZFCは無矛盾と仮定した上で、>>139 のような 考えはどうなのでしょうか？ どのみち独立性を示すためには基の論理体系が無矛盾であると 仮定しなければならないようなので。 150 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 00:01:06 ] 渕野昌先生、『ゲーデルと20世紀の論理学』で 御本人が執筆された公理的集合論の解説を丸々upされてるんですね。 太っ腹な御人だ。 151 名前：１３２人目の素数さん [2011/01/17(月) 18:09:18 ] >>149 ZFC集合論が矛盾していたとしても集合論は崩壊しないよ。 別の定式化をすれば良いだけだ。 152 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:08:31 ] 朝倉数学ハンドブックという本の飯高茂先生の章に 「P(N)の濃度をアレフ1と書く」 「アレフ0とアレフ1の間の濃度はないという主張を連続体仮説という」 （アレフは実際にはヘブライ文字で表記されています） と書いてあります。 連続体仮説が成り立たない場合にはアレフ0の次に アレフ(1/2)とかアレフεみたいな基数があるのだと思うのですが これは実数の集合で言うとどういったものになるんでしょうか？ 153 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:16:19 ] >>152 何世紀も引用されまくるような偉大な論文ができる。 154 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:53:22 ] >>151 しかし最定式化の段階で一旦ZFCに基づいていた証明を捨てなければなりませんよね。 そうなると数学全体をスクラップ＆ビルドしなおす必要が出てくると思います。 ある意味、集合論（数学の基礎）の崩壊かなと。 また、同等の機能を持った別の定式化というのは存在するでしょうか？ 同等の機能を持つなら同じ論理式が同じように証明できるわけで また矛盾してしまうのではと思います。 155 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:56:06 ] え？ 156 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:58:20 ] カントール以前には数学がなかったかのような言い分 157 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 19:59:01 ] ×言い分 ○言い様 158 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:01:46 ] >>154 その台詞自体があなたが基礎論のことを何もわかってないことを如実に示している ということを理解したほうが良い。 159 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:11:26 ] >>158 う〜ん。確かに基礎論難しくて良く分かってないけど 台詞のどの辺がだめなのか指摘してもらえたらいいな 160 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:12:19 ] 現代数学がZFCに基づいている、とはいっても 実際はZFCの表現力の一部しか使っていない。 再定式化する際には、数学に必要なだけの表現力を持つ体系であれば （ZFCをはじめとする集合論とは見た目が全然違っていても）何でもいい。 161 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:15:58 ] >>159 全部。学校のことを説明しているつもりで消防士の説明をしてるくらい根本的にオカシイ。 162 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:23:01 ] >>160 なるほど。サンクス。 崩壊は言い過ぎだったか。 既存の定理Ａと定理Ｂが衝突してどちらか捨てなければならない という事態なら生じるだろうか？ その場合でも、高校の様に（？）、数学Ａと数学Ｂに分かれて どちらも生き残るのだろうか… 163 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:42:35 ] せっかくの>>160も、バカを前に真意は伝わらずか。 164 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:47:37 ] >>162 既存の数学ってのはツーバイフォーの家みたいなもので、 その規格に合う基本部品さえ作れれば、 作る道具には依らないで同じ家ができるんだよ。 165 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 20:50:43 ] 実際の数学の"証明"は形式化されていないけど 形式化されていないからこそ融通が利く 166 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 21:08:23 ] すいませんが公理的集合論について詳しい和書ありますか？ できれば強制法や2階算術まで載っているのが良いんですが。 （キューネン以外で。 167 名前：162 mailto:sage [2011/01/17(月) 21:12:48 ] >>164 その代替部品って簡単に作れる（存在する）ものですか？ >>165 定理Ａと定理Ｂから矛盾が導けるとき もとの公理系から矛盾が導けるということだから 矛盾から任意の定理が導けるのは当たり前（？）で 単にもとの論理体系が矛盾するというだけか もとの論理体系を無矛盾なものに取り替えれば 定理Ａと定理Ｂがまた矛盾するかどうかは分からないわけか 現代の数学から見て明らかに矛盾するような 理論を作ったとしても、将来に論理の枠組みを変更して 無矛盾にできる可能性がずっと残されるのかな 168 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 21:17:55 ] >>166 こんなんありますよ ttp://kurt.scitec.kobe-u.ac.jp/~fuchino/misc/intro-to-set-theory-and-constructibility.pdf 169 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 21:28:05 ] 論理学にガロア理論（の類似物）ってありませんか？ 170 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 21:29:08 ] >>167 実数の話をしたいなら実数の公理を記述できるものを出せばいいけど それは別にZFCよりもずっと弱い系から出てくる理論なので余裕。 171 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 21:30:17 ] >>167 ゼロからきちんと勉強する気がないならあきらめろ、お前の考えは休むにも劣る。 172 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 22:13:09 ] 難波完爾の集合論があまりにもコンパクトに纏まってて泣ける 安いから損はしないけどね 173 名前：１３２人目の素数さん mailto:sage [2011/01/17(月) 22:38:38 ] >>170 >>171 先走りたがりなものでスミマセン ゼロから勉強する気はあります ありがとうございました また何かあったらよろしくお願いします 174 名前：１３２人目の素数さん mailto:sage [2011/01/21(金) 22:23:26 ] 命題論理の抽象の定義って何種類位知られているんでしょうか？ 175 名前：１３２人目の素数さん mailto:sage [2011/01/21(金) 22:50:24 ] (´･ω･)? 176 名前：１３２人目の素数さん mailto:sage [2011/01/21(金) 23:04:15 ] メレディスの公理系 A1 （（（（A→B）→（¬C→¬D））→C）→E）→（（E→A）→（D→A）） R1 A A→B├ B 177 名前：１３２人目の素数さん mailto:sage [2011/01/21(金) 23:31:57 ] ゲーデルによる高階論理を用いた自然数論の無矛盾性証明 が読める文献を御存知ありませんか？ 178 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 09:36:53 ] ウィキぺでぃあの証明論ひどすぎ ja.wikipedia.org/wiki/%E8%A8%BC%E6%98%8E%E8%AB%96 哲学系の人間が書いたに違いない 179 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 11:16:00 ] >>178 データ構造や自動定理証明や型理論など、 数学視点ではなく計算機科学視点が多いですが、 哲学視点はほとんどありません。 ひどいと感じたのはどこですか？ なぜ哲学系の人間が書いたと思ったのですか？ Proof theory (証明論の原文) en.wikipedia.org/wiki/Proof_theory 180 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 12:20:23 ] 俺もどこが酷いと思ったのか分からん 他のロジックの記事の方がよほど酷い 181 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 18:14:26 ] チャーチ・ロッサーの合流定理の証明ってどこかに載ってませんか？ 182 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 20:45:37 ] Barendregt嫁 183 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 22:59:33 ] 小野寛晰さんの本読んでんだけど、 テクニカルな議論と"意味"の解説の配分が絶妙だね ムラムラしてきたからオナヌして寝るわ 184 名前：１３２人目の素数さん mailto:sage [2011/01/22(土) 23:24:35 ] >>183 私もそれ今読んでます。 演習問題の質もちょうど良い。 国内の論理学入門書でも画期的なものだと思いますね。 今日明日で読了するつもりです。 185 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 00:03:22 ] >>183-184 この本ですか？ 現代数理論理学序説　(古森雄一・小野寛晰　著) www.amazon.co.jp/dp/4535785562 www.nippyo.co.jp/book/5333.html d.hatena.ne.jp/ytb/20100619/p2 186 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 01:35:03 ] その本は三章までは古森さんが書いてる 四章はあまり入門と言うような内容でもないし 「情報科学における論理」の方かと思った 187 名前：184 mailto:sage [2011/01/23(日) 10:10:24 ] 述語論理の意味論から急に難しくなってきた。 188 名前：184 mailto:sage [2011/01/23(日) 12:30:11 ] >>185 それだね。 日本の数理論理学の最高峰だと思う。 189 名前：183 mailto:sage [2011/01/23(日) 13:44:18 ] ありゃ、自分が今読んでるのは『情報科学のための論理』の方です もう一つの方もチェックしてみます 190 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 14:37:33 ] ＞『情報科学のための論理』 手触りが良くて、角ばってて、ガッシリしてて… とても良い本ですよね 191 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 15:22:51 ] >>189-190 『情報科学における論理』ですよね？ 情報科学における論理　(小野寛晰　著) www.amazon.co.jp/dp/4535608148 www.nippyo.co.jp/book/1292.html www10.atwiki.jp/shinsa/pages/49.html 192 名前：183 mailto:sage [2011/01/23(日) 15:37:19 ] >>191 あ、そうです。失礼しました。 193 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 21:04:17 ] 健全性と完全性を満たさない体系はどうなるの？ 194 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 21:14:53 ] pcf理論を哲でもわかる様に説明してちょんまげ。 195 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 22:44:08 ] もしも量化演算子に語られるものが 人間の脳の機能になければ、 あらゆるものは分類できず、すべてがバラバラであったであろう。 196 名前：１３２人目の素数さん mailto:sage [2011/01/23(日) 22:54:51 ] 竹内外史の実数論の無矛盾証明って『Proof Theory』以外 に載ってませんか？ 197 名前：184 mailto:sage [2011/01/23(日) 23:19:17 ] コンパクト性定理証明終了。 ようやくラムダ計算に突入。 198 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 00:00:36 ] ZFが無矛盾なのか気になって夜も眠れない・・・ぐぅ・・・ 199 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 03:19:30 ] >>196 "two application"になかったかなあ？ 200 名前：184 mailto:sage [2011/01/24(月) 07:08:31 ] >>198 ラムダ計算が矛盾したんだ。 ZFのだめだろう。 201 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 07:12:13 ] モノイド空間を定義して そこで健全性定理をイーストンの定理で導入すればZFが矛盾する。 202 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 12:04:44 ] >>199 あった 203 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 20:48:38 ] >>201 はいはいわろすわろす 204 名前：201 mailto:sage [2011/01/24(月) 23:07:59 ] >>203 > >>201 > はいはいわろすわろす バカにするわけじゃないけど、 これ俺の近所の小学生の会話の中にもあった（笑い 205 名前：201 mailto:sage [2011/01/24(月) 23:08:49 ] まぁ実際健全性定理が成立する体系なんてごくわずかな例外的な存在だけどなぁー。 206 名前：１３２人目の素数さん mailto:sage [2011/01/24(月) 23:33:57 ] 健全なんて幻想、セカイは不健全なものなのです。 207 名前：201 mailto:sage [2011/01/25(火) 23:54:05 ] 健全性定理と完全性定理が同時に成立しないということが、 ２階述語論理の第２不完全性定理の意味論。 208 名前：１３２人目の素数さん mailto:sage [2011/01/26(水) 19:40:32 ] 現代数理論理学序説の９３ページの 古典述語論理の体系が決定不可能であることの証明って、 不完全性定理と同等のものですよね？ 209 名前：１３２人目の素数さん mailto:sage [2011/01/26(水) 22:15:06 ] おもしろい講義ノートがあったので貼り貼り 様相論理と不完全性定理 ttp://www.shizuoka.ac.jp/~math/math/contents/kiroku/special/2006/shizuokashutyu.pdf

---

---

[ 続きを読む ] / [ 携帯版 ]

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