数学基礎論・数理論理学のスレッド その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/
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:020236１３２人目の素数さん
2011/01/29(土) 19:05:15Γ を空, A を px, B を ∀x px とする。条件がないとき, ⇒ の左側は正しい
が, 右側は正しくない。
0237１３２人目の素数さん
2011/01/30(日) 00:48:36px は一般には仮定「Г, px」に依存するから、実は一般化規則は使えなくて、
左辺も正しくない気がする。
0238１３２人目の素数さん
2011/01/30(日) 00:55:10⇒ の左側は正しい。
0239１３２人目の素数さん
2011/01/30(日) 01:09:39現代数理論理学序説に書いてある。
0240１３２人目の素数さん
2011/01/30(日) 03:32:49主流がどうのこうのと言ってる内は永遠の2番手ですよ
0241１３２人目の素数さん
2011/01/30(日) 21:24:01証明のツリーを１つ定めた上で、仮定の集合の元のうち、一般化規則の上式A が依存するものだけを問題にしていると思われ。
実際そう考えると、与えられたツリーを書きかえることで無条件に演繹定理は成り立つ。
ヒント：「Г, A ├ B」のツリーにおいて一般化規則を適用する際、
上式がAに依存する場合としない場合にわける。
依存する場合は「Aが閉論理式」と仮定したときと同様、
しない場合はツリーの上式から上の部分をそのまま利用して書きかえ。
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...
■ このスレッドは過去ログ倉庫に格納されています