数学基礎論・数理論理学のスレッド その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/
0242１３２人目の素数さん
2011/01/30(日) 21:24:08第1問って4番も正解でよくね？
ttp://www.moj.go.jp/content/000046586.pdf
0243１３２人目の素数さん
2011/01/30(日) 21:26:410244１３２人目の素数さん
2011/01/31(月) 00:07:41そもそも Г, A ├ B で A は仮定だよ。「A の依存する仮定」というの
がおかしいということいが分からないのかな。
0245１３２人目の素数さん
2011/01/31(月) 00:42:10演繹定理はヒルベルト流の体系についての定理である。ヒルベルト流の体系は
公理から定理を導くとき modus ponens と普遍化規則の二つの推論規則を使
う。証明図の頂上には公理しかないので普遍化規則には変数条件は必要ない。
しかし, 演繹定理を述べるためには頂上に公理以外のものを認める必要があ
る。頂上には公理以外のものを認め二つの推論規則を使って得られる図形
を「現代数理論理学序説」では証明図と区別して推論図と呼んでいる。
推論図においては証明図とは違って普遍化規則には変数条件が必要であると
「現代数理論理学序説」で述べられている。227 は変数条件は必要ないので
はないかと疑問を述べている。236 で述べたように変数条件をなくしてしま
うと演繹定理は成立しない。
「Г├ A」の意味は Г を頂上(頂上にある公理はГ に入れないでもよい )
とする A に至るヒルベルト流体系の推論図が存在する。頓珍漢なレスをし
ている人はこれが分かっていないのではないかな。
0246１３２人目の素数さん
2011/01/31(月) 03:08:250247ノニ
2011/01/31(月) 07:58:240248１３２人目の素数さん
2011/01/31(月) 12:21:50「A が依存する仮定」の「A」は「Г, A├ B」の「A」ではなく、
一般の状況での普遍化規則の上式のことだろう。
0249１３２人目の素数さん
2011/01/31(月) 12:31:15その目的が達成される限りにおいて、「仮定からの推論」には異なる定義があり得るということも覚えておくといいよ。
君の読んでる本では、
「個々の上式が依存する仮定」ではなく、
「あらかじめ与えられた集合の元すべてを仮定として考える」ようだけど、
それは議論を簡単にするためであり、
また、その程度の縛りがあっても十分有用な定理となるからだろう。
0250１３２人目の素数さん
2011/01/31(月) 12:45:07のだから, その本にしたがって答えるのが当然だろう。
0251１３２人目の素数さん
2011/01/31(月) 13:12:59ものと早とちりをしてしまったようだ。248 の指摘で早とちりに気づいた。
だとすると 227 での条件とは閉論理式という条件だけだ。そのような条件は
演繹定理にはないのが普通なので, 早とちりを引きずってしまった。
もちろん, 閉論理式という条件は必要ない。
0252１３２人目の素数さん
2011/01/31(月) 13:51:570253１３２人目の素数さん
2011/02/01(火) 13:14:264が駄目なのは、
問題文が「両立しないものを選べ」ではなく「否定を選べ」だから
0254１３２人目の素数さん
2011/02/03(木) 21:43:53ヒューズ／クレスウェル以外でなんかありませんか？
0255ノニ
2011/02/03(木) 22:36:23小野 寛晰
情報科学における論理 (情報数学セミナー)
0256１３２人目の素数さん
2011/02/05(土) 12:12:10ネット上にいっぱい転がってんの？
他の分野より多いよね
0257１３２人目の素数さん
2011/02/05(土) 19:37:12他分野のpdfファイルをあまり知らないだけでは
0258１３２人目の素数さん
2011/02/05(土) 21:05:40数理論理学って計算機科学の人のが詳しいってホント？
0259１３２人目の素数さん
2011/02/07(月) 20:59:150260１３２人目の素数さん
2011/02/07(月) 21:38:59あとCooperのcomputability theoryの新しい版が今度出るみたいよ
0261１３２人目の素数さん
2011/02/09(水) 19:58:22代数的な意味論って、完全性が成り立つように
無理矢理作った感じがするんですが、何か効用はあるんでしょうか。
0262１３２人目の素数さん
2011/02/09(水) 20:42:39作られたものなんで別に無理矢理じゃないと思うけど。
ハイティング代数の方は知らん
0263１３２人目の素数さん
2011/02/09(水) 22:22:000264１３２人目の素数さん
2011/02/09(水) 23:28:350265１３２人目の素数さん
2011/02/11(金) 01:26:29http://en.wikipedia.org/wiki/Pointless_topology とか
0266１３２人目の素数さん
2011/02/12(土) 02:18:220267１３２人目の素数さん
2011/02/12(土) 19:54:57無知乙。
インチキ扱いされるのは、
無限、宇宙、数学の基礎というワードに電波が群がっているから。
0268１３２人目の素数さん
2011/02/12(土) 22:15:21突然ですいませんがこれなんですか。
∀とか∃とかなんですか
テストなんです。助けて下さい
0269１３２人目の素数さん
2011/02/12(土) 22:57:02ttp://ja.wikipedia.org/wiki/%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
教科書読め。
0270１３２人目の素数さん
2011/02/13(日) 03:57:530271１３２人目の素数さん
2011/02/13(日) 04:32:230272１３２人目の素数さん
2011/02/13(日) 15:16:36[A]B⇒A
[B]A
この流れが全く分かりません。多分法則とか公式分かればとんでもなく簡単なんだろうけど。
明日本屋で勉強しようと思うんだが、なんかオススメの本ありますか？
0273１３２人目の素数さん
2011/02/13(日) 17:26:21「恒真式、真理表」を速攻理解しろ。
0274１３２人目の素数さん
2011/02/13(日) 19:03:51公理型に¬なんて含まれてたっけ？
0275１３２人目の素数さん
2011/02/13(日) 19:18:05公理図式の組にはバリエーションがあって、¬を含むタイプのもある。例えば
ルカシェヴィツの公理系L
公理１ A⊃（B⊃A）
公理２ （A⊃（B⊃C））⊃（（A⊃B）⊃（A⊃C））
公理３ （¬A⊃¬B）⊃（B⊃A）
推論規則１ A, A⊃B → B （MP）
0276１３２人目の素数さん
2011/02/13(日) 19:21:520277１３２人目の素数さん
2011/02/13(日) 19:22:07(A→(B→C))→((A→B)→(A→C))
(¬B→¬A)→((¬B→A)→B) 背理法
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
(¬B→¬A)→(A→B) 対偶律
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
¬¬A→A 二重否定除去（ただし¬AはA→⊥の略記）
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
((A→B)→A)→A パースの法則
etc...
0279１３２人目の素数さん
2011/02/13(日) 19:31:390280１３２人目の素数さん
2011/02/13(日) 20:20:540281１３２人目の素数さん
2011/02/13(日) 21:05:060282１３２人目の素数さん
2011/02/13(日) 21:38:410283１３２人目の素数さん
2011/02/13(日) 21:41:480284１３２人目の素数さん
2011/02/13(日) 21:44:020285１３２人目の素数さん
2011/02/13(日) 21:44:570286１３２人目の素数さん
2011/02/13(日) 21:48:39あ、そうか。サンクス。
0287１３２人目の素数さん
2011/02/13(日) 22:22:27> 自分が習った体系しか無いと思うとは、おめでたいやつだ。
他にあるってこと自体は知っていた。
ただ俺はHKといった。
HKは普通、
公理１ A→B→A
公理２ (A→B→C)→(A→B)→A→C
公理３ ((A→B)→A)→A
公理４ ¬→A
推論規則１ A, A⊃B → B （MP）
だろう？
今はBCIとかBCKとかBCKW...とか言われてるのを知らのか？
0288１３２人目の素数さん
2011/02/13(日) 22:27:43数学畑の人と哲学畑の人と両方教えて
0289１３２人目の素数さん
2011/02/13(日) 22:44:54集合論ならいるけど。
0290１３２人目の素数さん
2011/02/13(日) 22:49:33一応教えてください
0291１３２人目の素数さん
2011/02/13(日) 22:59:25ttp://twitter.com/#!/kururu_goedel
0292１３２人目の素数さん
2011/02/13(日) 23:59:220293１３２人目の素数さん
2011/02/14(月) 00:07:390294１３２人目の素数さん
2011/02/14(月) 00:09:130295１３２人目の素数さん
2011/02/14(月) 00:18:58DIAMOND: A PARADOX LOGIC (2ND EDITION) (Series on Knots & Everything)
http://www.amazon.co.uk/DIAMOND-PARADOX-LOGIC-Knots-Everything/dp/981428713X
この本で扱ってるDiamondって様相論理の可能性演算子と、
連続体仮説の一般化の方のとどちらでしょうか？
0296１３２人目の素数さん
2011/02/14(月) 01:14:20ドイツ語の頭文字をとって一部の教科書がそう読んでるだけじゃないの？
BCKとかのBとかCとかはそれぞれ一つの公理図式の名前だけどHKはそうじゃないでしょ。
松本和夫の本とかにもHKとか名付けてあるけど当時BCK論理とかがあったはずもないし。
一般的には、ほとんどの規則を推論規則として定式化する
Gentzenの自然演繹とかシーケント計算とかに対して
modus ponensとか汎化規則とかしか推論規則が無くて、
あとは公理として規則を立てるような体系のことをHilbertスタイルというように思う。
というか
＞公理４ ¬→A
これ意味分からんのだが。論理式になってないし。
0297１３２人目の素数さん
2011/02/14(月) 02:14:03> これ意味分からんのだが。論理式になってないし。
否定ではなくて、矛盾のつもりなのでしょう。
0298１３２人目の素数さん
2011/02/14(月) 23:24:240299１３２人目の素数さん
2011/02/15(火) 07:29:29・素朴集合論
・線形代数学
・位相空間論
・一階述語論理学
・グラフ理論
・群/体
・ルベーグ積分
・公理的な確率/統計
・関数論
などだ。難しいと感じるかは当人のセンス次第だ。
0300１３２人目の素数さん
2011/02/15(火) 09:25:54「難しい」と書いて「たのしい」と読むんだぞ
0301１３２人目の素数さん
2011/02/15(火) 09:27:020302１３２人目の素数さん
2011/02/15(火) 09:28:300303１３２人目の素数さん
2011/02/15(火) 11:44:47シェラハというイスラエルの爺さんの頭脳レベルを調べてみなされ。
0304１３２人目の素数さん
2011/02/15(火) 12:09:530305１３２人目の素数さん
2011/02/15(火) 12:14:05この文脈では、論文を量産できるほど簡単な分野であるかのようではないか
0306１３２人目の素数さん
2011/02/15(火) 12:15:20http://ja.m.wikipedia.org/wiki/サハロン・シェラハ?wasRedirected=true
0307１３２人目の素数さん
2011/02/15(火) 17:45:24「ラッセルのパラドックス」を解決した「グロタンディーク宇宙」とはどんなものなんですか？
ウィキ読んでもさっぱりわかりませんでした(笑)
0308１３２人目の素数さん
2011/02/15(火) 21:02:17どこで読んだのそれ？
0309１３２人目の素数さん
2011/02/15(火) 21:09:380310１３２人目の素数さん
2011/02/15(火) 21:11:35普通のZFでもラッセルのパラドクスは構成できないよ。
0311１３２人目の素数さん
2011/02/15(火) 21:24:20今ではそれに付け加えて、
・数論
・代数的トポロジー
・モデル理論
・チューリング/メドベージェフ還元
・計算量複雑性・再起理論
・不完全性定理（四則演算並みの頻度で多用）
・論理学の代数化定理周辺
までが求められる。
シェラーとかいう人は確か特異基数仮説周辺で有名な人じゃなかったっけ？
（私も全然ついていけてないです...
0312１３２人目の素数さん
2011/02/15(火) 21:29:100313１３２人目の素数さん
2011/02/15(火) 21:43:42なんで集合論に確率が必要なん？
てきとうに挙げただけちゃう？
0314１３２人目の素数さん
2011/02/15(火) 21:46:32カントール空間とかポーランド空間とか使うからでしょ。
メドヴェージェフ還元に＾＾
0315１３２人目の素数さん
2011/02/15(火) 21:57:460316１３２人目の素数さん
2011/02/15(火) 22:02:03メドベージェフ次数のおけるプールエルクリプキの定理に該当！
0317１３２人目の素数さん
2011/02/15(火) 22:19:310318１３２人目の素数さん
2011/02/15(火) 23:23:440319１３２人目の素数さん
2011/02/15(火) 23:27:250320１３２人目の素数さん
2011/02/16(水) 07:20:38シュプリンガーから
Kripke Models, Distributive Lattices, and Medvedev Degrees
Sebastiaan A. Terwijn
が出てる。
紙媒体は多分まだない。
0321１３２人目の素数さん
2011/02/16(水) 10:59:40ありがとうございます！
0322１３２人目の素数さん
2011/02/17(木) 17:43:46rankとdegreeについての二重帰納法を用いるものがありますよね？
証明図の変形によるrankとdegreeの減少を精密に評価することで、
何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、
どうも無理な気がしてきました。
実際どうなんでしょうか？
よろしければお知恵をお貸し下さい。
0323１３２人目の素数さん
2011/02/17(木) 19:03:27Girard の Proof theory and Logical comlpexity には
その方法で評価がされています。
また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の
自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ
ωを 3 に置き換えればよいというようなことが書いてあったと思います。
0324１３２人目の素数さん
2011/02/17(木) 20:36:27ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。
0325１３２人目の素数さん
2011/02/17(木) 23:25:04あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ？
0326１３２人目の素数さん
2011/02/18(金) 13:37:43なんでx=y→x'=y'じゃなくて
x'=y'→x=yなのか教えてください
0327１３２人目の素数さん
2011/02/18(金) 13:57:580328１３２人目の素数さん
2011/02/18(金) 15:47:050329１３２人目の素数さん
2011/02/18(金) 15:54:02演繹するか公理で仮定することになる。
0330１３２人目の素数さん
2011/02/18(金) 15:58:300331１３２人目の素数さん
2011/02/18(金) 16:28:40なにがいいの？
0332１３２人目の素数さん
2011/02/18(金) 16:43:54？
0333１３２人目の素数さん
2011/02/18(金) 16:47:140334１３２人目の素数さん
2011/02/18(金) 17:22:53〜じゃだめなの？＝〜でいいだろ。
ということだから、いいってのはどういう意味でいいっていってんのかってこと。
0335１３２人目の素数さん
2011/02/18(金) 19:20:420336１３２人目の素数さん
2011/02/18(金) 19:34:060337１３２人目の素数さん
2011/02/18(金) 19:39:50そんなうまく質問できるくらいなら質問してない
初めてペアノの公理見たんだよ
なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください
0338１３２人目の素数さん
2011/02/18(金) 19:47:260339１３２人目の素数さん
2011/02/18(金) 19:48:08これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。
0→1→2→3→1→2→3→1→2→3→…
形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。
上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。
0340１３２人目の素数さん
2011/02/18(金) 20:00:42x=y → x'=y'
ならば、
0→1→2→3→4
となるんじゃない？3の次は3'(=4)だけでしょ？
0341１３２人目の素数さん
2011/02/18(金) 20:06:45x'=y'→x=yを仮定しないと、3' が 1 になり得るという話
■ このスレッドは過去ログ倉庫に格納されています