数学基礎論・数理論理学のスレッド その7
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2010/11/11(木) 22:13:5719世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学のスレッド その6
http://kamome.2ch.net/test/read.cgi/math/1265884076/
0135１３２人目の素数さん
2011/01/15(土) 06:04:33もっと真剣に考えないといけないと思うようになりました
真とも偽とも判断が付かない命題があるなら
真か偽かを考えると同時に証明できない可能性も考えるべきだと思います
そこで、ある命題が「真とも偽とも証明できない」ことを
証明するような手段を知りたいのですが、
何か手順・プログラムなどがあったら教えてください
0136１３２人目の素数さん
2011/01/15(土) 08:31:57集合論的な独立命題なら強制法使って独立性示したり
他の良く分かっている命題に帰着させたりとか。
0137135
2011/01/15(土) 18:53:51強制法とか参考になります
自分はそれほど論理学をマスターしていないので
もう少し詳しく教えていただけるとありがたいです
> 反例を作るとか。
これはどのような反例を作ればよいのでしょう？
真または偽と証明できたと仮定して反例を導くのでしょうか？
しかし不完全性の例だと、真であっても偽であっても
矛盾しないような気がします。
> 集合論的な独立命題なら強制法使って独立性示したり
強制法をいまチラ見しただけでまだよく分かってないのですが
任意の命題（集合論的な独立命題でないもの）に対しては
適用できない手法ですか？
よろしくお願いいたします
0138１３２人目の素数さん
2011/01/15(土) 19:58:30とか言った場合にAを満たす例とnot Aの例の両方を作るとか。
強制法が適用できないような独立命題もあって良さそうなものだけど、
現実問題としてはあまりそういうものは知られてないんじゃないかと思う。
だから独立性のことが気になるなら強制法が一番強力な武器なのは間違いないと思う。
ロジックでは強制法が使えないほど弱い理論（たとえば限定算術）から或る定理が
独立かどうかとかが問題になることもあるのだけど、
普通の数学ではZFCから証明出来たら、証明できたものと見做す。
だいたいAもnot Aも証明できないというのが真実だとしても、
「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。
0139１３２人目の素数さん
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段階、ω^ω段階のようなことを妄想します。
これらの可能性を包括的に走査するプログラムなどを当方は妄想していますが
不完全性からは無謀な試みでしょうか？
0140１３２人目の素数さん
2011/01/15(土) 21:46:210141１３２人目の素数さん
2011/01/15(土) 21:53:19いまのところ戸田先生の『論理学をつくる』をざっと眺めました。
他の論理学の本は、なんだか頭に入ってこないというか、
書き方が難しいです。哲学よりの本も多いし…
数理論理学をやるのによい中級の本はないでしょうか？
0142１３２人目の素数さん
2011/01/15(土) 21:55:34……なぜかと言うと、矛盾からは任意の命題が出て来るので、
Tから証明できない或る命題が存在する⇔Tが無矛盾
よって、たとえばZFCで考えているとして、ZFCが無矛盾であることが証明できない限り
三段目以降は全部自動的に無理になってしまう。
これも前のスレにあった話だけど。
やっぱ皆考えることは同じだよね。
0143１３２人目の素数さん
2011/01/15(土) 22:02:29自分は『論理学をつくる』の次に
前原昭二『数学基礎論入門』を読みました。
論理計算を実践しつつ（かなり丁寧）、不完全性定理の厳密な証明が学べます。
命題論理の公理系から始まるので、シンタクスとセマンティクスの区別さえできていれば、
他に予備知識は不要な本です。
0144１３２人目の素数さん
2011/01/15(土) 22:32:41たぶんその栄養が身になるころにはなんのために論理学を身に着けようとしたのか
もう忘れてしまっているのに十分な時間が経過していることでしょう。
三途の川の向こうに答えがあるかもしれませんね。
0145１３２人目の素数さん
2011/01/15(土) 22:48:53そうですか…
しかしZFCからは連続体仮説が証明できない、という結果があったと思いますが
これはZFCが無矛盾であることを示したことにならないでしょうか？
もっと込み入った事情がありますか？
0146１３２人目の素数さん
2011/01/15(土) 22:51:39ありがとうございます
その本も手元に持っていたので読み込んでみます
>>144
まあ数学やる以上は答えが出るか分からない旅…
0147１３２人目の素数さん
2011/01/16(日) 00:43:48> これはZFCが無矛盾であることを示したことにならないでしょうか？
そうするとZFCは無矛盾でないことになりますので、大発見だと思います。
0148１３２人目の素数さん
2011/01/16(日) 10:30:53単純に、ZFCが無矛盾だとすれば、の前提つきでの話。
もちろん、矛盾していても証明できるけど。
0149139
2011/01/16(日) 18:36:25なるほど。
よく言われる「連続体仮説は証明も反証もできない命題である」
ということの証明には前提条件があったのですね。
しかしZFCが矛盾するとすると集合論が崩壊するので
数学は致命的なダメージを受けますね。
数学という船にのっている以上、ZFCは無矛盾、と仮定するのは
自然な成り行きだと思います。
言い方は悪いですが、沈むときは一緒だ、みないな。
そこでZFCは無矛盾と仮定した上で、>>139 のような
考えはどうなのでしょうか？
どのみち独立性を示すためには基の論理体系が無矛盾であると
仮定しなければならないようなので。
0150１３２人目の素数さん
2011/01/17(月) 00:01:06御本人が執筆された公理的集合論の解説を丸々upされてるんですね。
太っ腹な御人だ。
0151１３２人目の素数さん
2011/01/17(月) 18:09:18ZFC集合論が矛盾していたとしても集合論は崩壊しないよ。
別の定式化をすれば良いだけだ。
0152１３２人目の素数さん
2011/01/17(月) 19:08:31「P(N)の濃度をアレフ1と書く」
「アレフ0とアレフ1の間の濃度はないという主張を連続体仮説という」
（アレフは実際にはヘブライ文字で表記されています）
と書いてあります。
連続体仮説が成り立たない場合にはアレフ0の次に
アレフ(1/2)とかアレフεみたいな基数があるのだと思うのですが
これは実数の集合で言うとどういったものになるんでしょうか？
0153１３２人目の素数さん
2011/01/17(月) 19:16:19何世紀も引用されまくるような偉大な論文ができる。
0154１３２人目の素数さん
2011/01/17(月) 19:53:22しかし最定式化の段階で一旦ZFCに基づいていた証明を捨てなければなりませんよね。
そうなると数学全体をスクラップ＆ビルドしなおす必要が出てくると思います。
ある意味、集合論（数学の基礎）の崩壊かなと。
また、同等の機能を持った別の定式化というのは存在するでしょうか？
同等の機能を持つなら同じ論理式が同じように証明できるわけで
また矛盾してしまうのではと思います。
0155１３２人目の素数さん
2011/01/17(月) 19:56:060156１３２人目の素数さん
2011/01/17(月) 19:58:200157１３２人目の素数さん
2011/01/17(月) 19:59:01○言い様
0158１３２人目の素数さん
2011/01/17(月) 20:01:46その台詞自体があなたが基礎論のことを何もわかってないことを如実に示している
ということを理解したほうが良い。
0159１３２人目の素数さん
2011/01/17(月) 20:11:26う〜ん。確かに基礎論難しくて良く分かってないけど
台詞のどの辺がだめなのか指摘してもらえたらいいな
0160１３２人目の素数さん
2011/01/17(月) 20:12:19実際はZFCの表現力の一部しか使っていない。
再定式化する際には、数学に必要なだけの表現力を持つ体系であれば
（ZFCをはじめとする集合論とは見た目が全然違っていても）何でもいい。
0161１３２人目の素数さん
2011/01/17(月) 20:15:58全部。学校のことを説明しているつもりで消防士の説明をしてるくらい根本的にオカシイ。
0162１３２人目の素数さん
2011/01/17(月) 20:23:01なるほど。サンクス。
崩壊は言い過ぎだったか。
既存の定理Ａと定理Ｂが衝突してどちらか捨てなければならない
という事態なら生じるだろうか？
その場合でも、高校の様に（？）、数学Ａと数学Ｂに分かれて
どちらも生き残るのだろうか…
0163１３２人目の素数さん
2011/01/17(月) 20:42:350164１３２人目の素数さん
2011/01/17(月) 20:47:37既存の数学ってのはツーバイフォーの家みたいなもので、
その規格に合う基本部品さえ作れれば、
作る道具には依らないで同じ家ができるんだよ。
0165１３２人目の素数さん
2011/01/17(月) 20:50:43形式化されていないからこそ融通が利く
0166１３２人目の素数さん
2011/01/17(月) 21:08:23できれば強制法や2階算術まで載っているのが良いんですが。
（キューネン以外で。
0167162
2011/01/17(月) 21:12:48その代替部品って簡単に作れる（存在する）ものですか？
>>165
定理Ａと定理Ｂから矛盾が導けるとき
もとの公理系から矛盾が導けるということだから
矛盾から任意の定理が導けるのは当たり前（？）で
単にもとの論理体系が矛盾するというだけか
もとの論理体系を無矛盾なものに取り替えれば
定理Ａと定理Ｂがまた矛盾するかどうかは分からないわけか
現代の数学から見て明らかに矛盾するような
理論を作ったとしても、将来に論理の枠組みを変更して
無矛盾にできる可能性がずっと残されるのかな
0168１３２人目の素数さん
2011/01/17(月) 21:17:55こんなんありますよ
ttp://kurt.scitec.kobe-u.ac.jp/~fuchino/misc/intro-to-set-theory-and-constructibility.pdf
0169１３２人目の素数さん
2011/01/17(月) 21:28:050170１３２人目の素数さん
2011/01/17(月) 21:29:08実数の話をしたいなら実数の公理を記述できるものを出せばいいけど
それは別にZFCよりもずっと弱い系から出てくる理論なので余裕。
0171１３２人目の素数さん
2011/01/17(月) 21:30:17ゼロからきちんと勉強する気がないならあきらめろ、お前の考えは休むにも劣る。
0172１３２人目の素数さん
2011/01/17(月) 22:13:09安いから損はしないけどね
0173１３２人目の素数さん
2011/01/17(月) 22:38:38>>171
先走りたがりなものでスミマセン
ゼロから勉強する気はあります
ありがとうございました
また何かあったらよろしくお願いします
0174１３２人目の素数さん
2011/01/21(金) 22:23:260175１３２人目の素数さん
2011/01/21(金) 22:50:240176１３２人目の素数さん
2011/01/21(金) 23:04:15A1 （（（（A→B）→（¬C→¬D））→C）→E）→（（E→A）→（D→A））
R1 A A→B├ B
0177１３２人目の素数さん
2011/01/21(金) 23:31:57が読める文献を御存知ありませんか？
0178１３２人目の素数さん
2011/01/22(土) 09:36:53http://ja.wikipedia.org/wiki/%E8%A8%BC%E6%98%8E%E8%AB%96
哲学系の人間が書いたに違いない
0179１３２人目の素数さん
2011/01/22(土) 11:16:00データ構造や自動定理証明や型理論など、
数学視点ではなく計算機科学視点が多いですが、
哲学視点はほとんどありません。
ひどいと感じたのはどこですか？
なぜ哲学系の人間が書いたと思ったのですか？
Proof theory (証明論の原文)
http://en.wikipedia.org/wiki/Proof_theory
0180１３２人目の素数さん
2011/01/22(土) 12:20:23他のロジックの記事の方がよほど酷い
0181１３２人目の素数さん
2011/01/22(土) 18:14:260182１３２人目の素数さん
2011/01/22(土) 20:45:370183１３２人目の素数さん
2011/01/22(土) 22:59:33テクニカルな議論と"意味"の解説の配分が絶妙だね
ムラムラしてきたからオナヌして寝るわ
0184１３２人目の素数さん
2011/01/22(土) 23:24:35私もそれ今読んでます。
演習問題の質もちょうど良い。
国内の論理学入門書でも画期的なものだと思いますね。
今日明日で読了するつもりです。
0185１３２人目の素数さん
2011/01/23(日) 00:03:22この本ですか？
現代数理論理学序説 (古森雄一・小野寛晰 著)
http://www.amazon.co.jp/dp/4535785562
http://www.nippyo.co.jp/book/5333.html
http://d.hatena.ne.jp/ytb/20100619/p2
0186１３２人目の素数さん
2011/01/23(日) 01:35:03四章はあまり入門と言うような内容でもないし
「情報科学における論理」の方かと思った
0187184
2011/01/23(日) 10:10:240189183
2011/01/23(日) 13:44:18もう一つの方もチェックしてみます
0190１３２人目の素数さん
2011/01/23(日) 14:37:33手触りが良くて、角ばってて、ガッシリしてて…
とても良い本ですよね
0191１３２人目の素数さん
2011/01/23(日) 15:22:51『情報科学における論理』ですよね？
情報科学における論理 (小野寛晰 著)
http://www.amazon.co.jp/dp/4535608148
http://www.nippyo.co.jp/book/1292.html
http://www10.atwiki.jp/shinsa/pages/49.html
0193１３２人目の素数さん
2011/01/23(日) 21:04:170194１３２人目の素数さん
2011/01/23(日) 21:14:530195１３２人目の素数さん
2011/01/23(日) 22:44:08人間の脳の機能になければ、
あらゆるものは分類できず、すべてがバラバラであったであろう。
0196１３２人目の素数さん
2011/01/23(日) 22:54:51に載ってませんか？
0197184
2011/01/23(日) 23:19:17ようやくラムダ計算に突入。
0198１３２人目の素数さん
2011/01/24(月) 00:00:360199１３２人目の素数さん
2011/01/24(月) 03:19:30"two application"になかったかなあ？
0201１３２人目の素数さん
2011/01/24(月) 07:12:13そこで健全性定理をイーストンの定理で導入すればZFが矛盾する。
0202１３２人目の素数さん
2011/01/24(月) 12:04:44あった
0203１３２人目の素数さん
2011/01/24(月) 20:48:38はいはいわろすわろす
0205201
2011/01/24(月) 23:08:490206１３２人目の素数さん
2011/01/24(月) 23:33:570207201
2011/01/25(火) 23:54:05２階述語論理の第２不完全性定理の意味論。
0208１３２人目の素数さん
2011/01/26(水) 19:40:32古典述語論理の体系が決定不可能であることの証明って、
不完全性定理と同等のものですよね？
0209１３２人目の素数さん
2011/01/26(水) 22:15:06様相論理と不完全性定理
ttp://www.shizuoka.ac.jp/~math/math/contents/kiroku/special/2006/shizuokashutyu.pdf
0210１３２人目の素数さん
2011/01/26(水) 22:16:020211１３２人目の素数さん
2011/01/26(水) 22:25:06>>208
同等というと語弊がある気がするけど
不完全性定理を使って示すよね
0212１３２人目の素数さん
2011/01/26(水) 22:30:34定理3.1.13が不完全性定理でしょうか？
この本は不完全性定理という記述をあえて避けているんでしょうか。
とすると、論理学の古典や歴史的文脈は完ぺきに排除した、
天下り的現代論理学入門書ということになるのでしょうか。
0213１３２人目の素数さん
2011/01/26(水) 22:42:26その定理3.1.13 のステイトメントをここに書いた方が早い気がする
0214１３２人目の素数さん
2011/01/26(水) 22:48:27定理3.1.13
空でないCL-項の集合AがCL-項全体ではなく、
Weak-equalityについて閉じているならば、
CL-項が集合Aに入っているかを判定する決定手続きは存在しない。
0215１３２人目の素数さん
2011/01/26(水) 22:53:350216１３２人目の素数さん
2011/01/27(木) 11:39:27> 古典述語論理の体系が決定不可能であることの証明って、
> 不完全性定理と同等のものですよね？
全く違います
0217１３２人目の素数さん
2011/01/27(木) 19:06:24概念？ 論理の記号操作？
0218１３２人目の素数さん
2011/01/27(木) 19:07:050219１３２人目の素数さん
2011/01/27(木) 20:06:47イングランド出身の傭兵で中世イタリアの伝説的英雄、
ジョン・ホークウッドによると、占領地で女達を輪姦し続けると、
だいたい30人くらいで必ず死んでしまうらしい。
商売ならなんでもなくても命がどうなるかわからない状況で、
輪姦され続けると興奮し過ぎで必ず死ぬらしい。
これ、豆知識な。
0220１３２人目の素数さん
2011/01/27(木) 20:08:380221１３２人目の素数さん
2011/01/27(木) 20:11:04違うなら何だというのだ？
0222１３２人目の素数さん
2011/01/27(木) 20:12:51明日、塾の生徒に教えてやろうっと
0223１３２人目の素数さん
2011/01/27(木) 22:29:06直観主義命題論理
超直観主義命題論理
：
：
中間論理
：
：
古典命題論理
0224１３２人目の素数さん
2011/01/28(金) 00:56:41それも解らないんなら数理論理学の基本から勉強し直せ
0225１３２人目の素数さん
2011/01/28(金) 07:25:34だから今数理論理学の入門書を読んでいる。
私は不完全性定理については全く知らないが、
名前だけは聞いたことがある。
だからこそ定理3.1.13が不完全性定理というものなのかと聞いている。
0226１３２人目の素数さん
2011/01/28(金) 08:49:39チホノフの定理とツォルンの補題が違うのと同じくらいには違う
同等だと言えば同等だけど違うと言えば違う
不完全性定理のステートメントも知らんのに
>>212みたいなこと言うと誤解呼ぶと思うなあ
別にそんなに天下り的じゃないよ
ロジックはシンタックスだけ先にあって後から意味論が考えられるようなことが良くある
組合せ論理はそうじゃないと思うけど、これは初学者がシンタックスと意味論を
混同するようなことがあるから敢えてそれがないようにこういう導入の仕方を取っているだけ
0227１３２人目の素数さん
2011/01/28(金) 14:18:32Γ, A├ B ⇒ Γ├ A→B
（一般化規則 「A から ∀xA を導いてよい」 を適用する際、
x は A が依存する仮定に自由変数として現れないものとする）
なんですけど、
Γの元や A が閉論理式である、
といったような仮定無しに無条件に成り立ちますよね？
0228１３２人目の素数さん
2011/01/28(金) 21:29:52シンタックスだけで意味論が見つかっていない
論理学って何があるの？
0229ノニ
2011/01/28(金) 21:33:090230１３２人目の素数さん
2011/01/28(金) 22:09:16Scottが考えたんだったと思う
>>229
無い
0231ノニ
2011/01/28(金) 23:17:100232１３２人目の素数さん
2011/01/29(土) 00:10:10代数的論理学は入門書どころか
基本的文献が1冊しかないのでは？
代数的方法による論理学の新たな展開
http://kaken.nii.ac.jp/d/p/17540109
>代表者 2005年度〜2007年度 小野 寛晰
代数的視点からの論理へのアプローチ (小野寛晰)
http://www.jaist.ac.jp/~mizuhito/ppl_ss07/OHP/msj07.pdf
>また、部分構造論理に対する代数的研究におけるこれまでの成果を共著としてまとめ、
>この春に"Residuated Lattices: an algebraic glimpse at substructural logics"として出版する。
>ここではこのような研究のことを、従来のabstract algebraic logicよりは
>広い意味に解釈して代数的論理学とよぶことにする。
Residuated Lattices: An Algebraic Glimpse at Substructural Logics
http://www.amazon.co.jp/dp/0444521410
0233１３２人目の素数さん
2011/01/29(土) 00:34:300234ノニ
2011/01/29(土) 13:39:27世界的に abstract algebraic logic と modal logic の
2本柱なのに、大丈夫なのかね、この国は。
意味論もウィトゲンシュタイン流の2値論理は終焉を迎えて、
真理値がノルム空間に拡張された fuzzy logic の
萌芽も見え始めているというのに・・・。
0235１３２人目の素数さん
2011/01/29(土) 17:22:02■ このスレッドは過去ログ倉庫に格納されています