数学基礎論・数理論理学 その12
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2012/03/24(土) 09:46:09.5319世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学 その11
http://uni.2ch.net/test/read.cgi/math/1325513069/
0153151
2012/04/12(木) 08:42:55.52ありがとうございます。でも
本の通り書いたので省略はないです。
仮に(1)(2)(3)のす
べてを満たすならという意味を著者がこめてたとしてもよくわからないです
何回も、本を見返したりしました。
自分のカッコの付け方がおかしかったかと思いかえてみたりしましたがわかりません
ありがとうございました
0154１３２人目の素数さん
2012/04/12(木) 10:03:02.98そういうことなら、本の記述が不適切であり、
あなたの「最初の『Ａ∧』についてどうも理解できない」は正しい
反応だと思う。
0155１３２人目の素数さん
2012/04/12(木) 18:37:06.08という話、僕はむしろ逆だと思うけどな。
メタ理論ZFCの中でメタ理論ZFCそのもののモデルを作ったり、
メタ理論に独立な命題を加えたり外したりで、
集合論ではメタ理論を気にしなければいけないので、通常の数学とは毛色が全然違う。
非古典論理ではメタ理論なんて気にもせずに、
群や環などの代数系を扱うのと同じように○○論理の代数系を扱うだけ。
非古典論理の方がずっと普通の数学の匂いがする。
0156あのこうちやんは始皇帝だった
2012/04/12(木) 19:36:47.85お前たちは、定職に就くのが先決だろがああああああ！！！！！！！！！！！！！
ニート・無職の、ゴミ・クズ・カスのクソガキどもがああああああ！！！！！！！！！
0157１３２人目の素数さん
2012/04/12(木) 19:42:57.33, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0158１３２人目の素数さん
2012/04/12(木) 22:45:50.60私は非古典論理が代数構造だけ研究しているとは思いません。
0159１３２人目の素数さん
2012/04/13(金) 03:18:50.99メタ理論を気にしなくていいというのは（ほとんどの場合）確か。
だから大筋としては>>155に同意。
「通常の数学」から奇異の目で見られる一番の原因は
メタ理論を気にしたり独立命題とか扱っているからだと思うので。
0160１３２人目の素数さん
2012/04/13(金) 08:31:27.42非古典論理というと代数というイメージが強いですね。
0161１３２人目の素数さん
2012/04/13(金) 21:51:50.25命題論理の演繹が健全であることは、有限の範囲
であれば真理値表を作れば明らかだと思います。
しかし、妥当式ならば演繹が存在するのか?
つまり、証明できるのかと聞かれると途端に
分からなくなります。
古典論理ならば全ての妥当式に演繹が存在するそうですが、
使用する結合記号を限定してしまえば、直観主義論理でも
完全なのでしょうか?
結合記号¬→のみで表される命題が妥当式ならば、
同一律とprinciple of explosionのみを公理とする推論体系で
証明可能なのでしょうか？
たとえば、
((A→((B→C)→C))→((B→C)→C))→(
(A→((B→C)→C))→((B→((A→C)→C))→(
(A→(B→C))→((C→((A→B)→B))→(
(A→(C→B))→((B→(C→A))→(
(A→(B→¬C)))))))))
は、同一律とprinciple of explosionのみで証明可能なのでしょうか?
言い換えれば、結合記号¬→のみで表される命題が妥当式ならば、
¬→⊥の導入と除去のみで証明図が示せるのでしょうか?
もし良ければ、教えてください。
0162１３２人目の素数さん
2012/04/13(金) 22:10:09.34かなりの部分が命題の独立性証明にあると思うけどなあ
それに集合論のひとは案外、外の人が思うよりも
群論や環論の公理系と似たようにZFCの公理系やそのモデルなどを扱っていると思う。
メタ理論と意味論を与える理論の区別をきちんとしていれば、
原理的にはほぼ全てのケースで、集合論における独立性証明を行うときの
メタ理論は弱い自然数論と見做せる。
一方で時相論理とか義務論理とかの研究の興味は
体系の数学的性質にはあまり無いと思う
0163１３２人目の素数さん
2012/04/13(金) 22:12:34.22その場合、可能世界意味論などの、古典論理の場合とは異なる意味論を採用しなければなりません
直観主義論理における「妥当式」というのはどういったものを考えていますか？
0164１３２人目の素数さん
2012/04/13(金) 22:24:45.00古いのでも新しいのでもたくさんお願いします
0165１３２人目の素数さん
2012/04/13(金) 22:28:38.57Elliott Mendelson INTRO..MATHEMATICAL LOGIC
0166１３２人目の素数さん
2012/04/13(金) 22:40:19.65ありがとうございます
これはもしかして英語で書かれてますか？
自分は英語さっぱりわかりません
0167１３２人目の素数さん
2012/04/13(金) 22:45:05.83もちろん、数学的な内容まで楽に理解できるわけではありませんが
0168１３２人目の素数さん
2012/04/13(金) 22:49:58.55それがよく分からないのです。
だから、結合記号¬→のみで表される命題が妥当式ならば
直観主義論理の範囲で証明できるのか？
と言う疑問が沸きました。
0169１３２人目の素数さん
2012/04/13(金) 22:51:45.72日本語で書かれたのがいいです
0170１３２人目の素数さん
2012/04/14(土) 00:01:39.40あなたが何に疑問を抱いているか、いまひとつわからないけれども、次の事実はご存知ですか？
パースの論理式と呼ばれる
((A→B)→A)→A
はトートロジーであるが、直観主義論理では証明できない。
（A,Bは異なる命題変数）
0171１３２人目の素数さん
2012/04/14(土) 00:07:02.30私は非古典論理が時相論理とか義務論理とかだけ研究しているとは思いません。
上で名前の挙がった小野先生の論文を幾つか見られては？
0172１３２人目の素数さん
2012/04/14(土) 00:15:19.59モデル検査などの応用指向で時相論理を研究する人や、
哲学指向の論理学で義務論理を研究する人はそうでしょう。
しかし、様々な代数系の数学的性質を調べるのと同様に、
時相論理や義務論理の数学的性質プロパーに興味をもって
研究している非古典論理研究者もいるのではないでしょうか。
それにどれだけの意義があるかは別問題として。
0173１３２人目の素数さん
2012/04/14(土) 00:21:16.870174１３２人目の素数さん
2012/04/14(土) 01:46:53.59>かなりの部分が命題の独立性証明にあると思うけどなあ
これって>>86や>>105の言ってる集合論の「論理学」の側面だな
0175１３２人目の素数さん
2012/04/14(土) 01:49:43.980176１３２人目の素数さん
2012/04/14(土) 01:59:25.38連続体仮説がZFCから独立という話は全然毛色の違う話だと思うが
0177１３２人目の素数さん
2012/04/14(土) 02:18:11.46どう違うのかkwsk
0178１３２人目の素数さん
2012/04/14(土) 02:24:29.16連続体仮説の独立性では ZFC + CH と ZFC + ¬CH のモデルを ZFC の中で構成する。
ユークリッド幾何学の公理のモデルは、どこで構成するか気にする必要は余りない。
0179１３２人目の素数さん
2012/04/14(土) 02:32:01.120180１３２人目の素数さん
2012/04/14(土) 02:38:37.45それは瑣末な問題にしか見えないが？
0181１３２人目の素数さん
2012/04/14(土) 07:05:21.280182１３２人目の素数さん
2012/04/14(土) 07:11:14.28やっぱり、((A→B)→A)→A は証明できないんですね。
納得できました。ありがとうございます。
0183１３２人目の素数さん
2012/04/14(土) 07:17:32.96dentialって言われる記号1つのやり方も存在するよ。
記号が理論からどれだけ減らせるかは問題じゃないよ。
0184165
2012/04/14(土) 07:39:34.76英語じゃなくてプログラミング言語だと思えばどうでしょう？
決まりきった言い回ししか出てこないので。
ttp://homepage2.nifty.com/PAF00305/math/writing.html
上記サイトとForestという英文法書と電子辞書（WEB上のでもOK）を使用して
できれば洋書で学習してください。
演習を解くならほとんど文章を熟読する必要もありませんし。
あとはWEB上のPDFで同じ部分の日本語で書かれたものと比較しながら進めてください。
和書で学習する方が上記のやり方よりも最終的に遠回りになります。
現時点で独習可能でまともな論理学入門書は日本では出版されていません。
0185１３２人目の素数さん
2012/04/14(土) 07:52:03.52最近は和書でも結構良い本が出てるけどね
0186１３２人目の素数さん
2012/04/14(土) 08:02:20.59横レスだが、同じ独立命題と言っても、
例えば交換法則が群の公理から独立というのと
連続体仮説が「通常の数学すべて」から独立というのとでは、
「通常の数学」の人からの気色の悪さはまるっきり違うと思う。
0187１３２人目の素数さん
2012/04/14(土) 08:06:37.79どうも作用素環論とか離散群論の微妙な問題だと、連続体仮説が効いてくるらしい。
0188１３２人目の素数さん
2012/04/14(土) 08:14:41.97そうして集合論者は喜び勇んで駆けつけるが、
作用素環論者や離散群論者は色々理由をつけて避けようとするわけだ。
いつまで経ってもロジシャン側から「通常の数学者」への片思い。
0189１３２人目の素数さん
2012/04/14(土) 08:56:20.550190１３２人目の素数さん
2012/04/14(土) 09:01:57.82>>188
そういう意味では >>172 の言う非古典論理研究者の方は
「ある論理が決定可能」という数学的性質を証明すると
それに興味を持ってくれる応用指向研究者がいるはずなので、
「ロジシャンから通常の数学者への片思い」よりは幸せか？
0191１３２人目の素数さん
2012/04/14(土) 09:02:26.33以前、つまり、20年以上前はそういってもおかしくなかったと思う。
最近は、通常の数学者風の集合論者だか、集合論者風の通常数学者がいる。
0192169
2012/04/14(土) 10:14:23.66丁寧にありがとうございます
0193１３２人目の素数さん
2012/04/14(土) 14:03:26.49差し支えなければ具体的な研究者名を挙げていただけませんか。
決して「誹謗中傷」には当たらないと思いますので。
0194１３２人目の素数さん
2012/04/14(土) 16:22:53.39昔から基礎論に興味を示す奇特な「通常の数学」者は少数ながらいた。
現在、そういう奇特な人間が数人いたところで事情は昔と変わらない。
0195１３２人目の素数さん
2012/04/14(土) 17:59:51.59小野先生の専門である部分構造論理の代数的研究では代数屋さんとの交流がずっと続いていますよ
0196１３２人目の素数さん
2012/04/14(土) 18:26:13.58持論が先に有って、どんな事象を突き付けられても頑強に受け入れを拒否している感じ。
0197１３２人目の素数さん
2012/04/14(土) 18:30:42.16数学が物理に応用されるからといって、数学が物理になるわけではないよね
>>191
物理学者風の数学者や数学者風の物理学者がいるからといって、数学が物理になるわけではないよね
>>195
物理との交流があるからといって、数学が物理になるわけではないよね
0198１３２人目の素数さん
2012/04/14(土) 18:35:12.25話は簡単で>>191がそういう研究者がいるだけではなく、
それが大きな潮流になっているという事象を突きつければいいだけのこと。
0199１３２人目の素数さん
2012/04/14(土) 18:59:21.43大きな潮流かどうかはそれで分かるだろうから。
0200187
2012/04/14(土) 19:32:56.50応用というのとは違うみたい。
0201１３２人目の素数さん
2012/04/14(土) 19:35:27.10大きな潮流なんてどうとでも言えるからねえ。
0202１３２人目の素数さん
2012/04/14(土) 20:07:34.17反駁不可能なくらいの決定的証拠を期待しようじゃないの
0203１３２人目の素数さん
2012/04/14(土) 20:30:28.030204１３２人目の素数さん
2012/04/15(日) 00:03:26.75設立準備委員会ができたという話は聞いたのですが、いつ正式に出来るのでしょうか？
0205１３２人目の素数さん
2012/04/15(日) 20:31:49.29任意の論理式ψについて、¬¬ψが直観主義論理において証明不可能ならば、古典論理においても
妥当式ではないと言えるのでしょうか?
((A→B)→A)→A は証明できないとしても、¬¬(((A→B)→A)→A)は
証明できますよね？
あと、A→¬¬Aは最小論理で証明できるので、ψが直観主義論理で
証明できるなら、¬¬ψも直観主義論理で証明できるのでしょうか?
(少なくとも、¬¬(A→A)は、証明できますよね・・・)
ならば、
結合記号¬→のみで表される命題Pが妥当式ならば、
¬¬Pは、結合記号¬→⊥の導入と除去だけで、
証明図を示せるのでしょうか?
0206１３２人目の素数さん
2012/04/15(日) 22:32:48.96あなたの言っていることは、まさに有名なグリベンコの定理ではないでしょうか：
【グリベンコの定理】
任意の命題論理式 A に関して次の２条件は同値：
（１） A が古典論理で証明可能。
（２） ¬¬A が直観主義論理で証明可能。
0207１３２人目の素数さん
2012/04/16(月) 20:39:17.10私の知識の7割は日本版Wikipediaなので・・・orz
0208１３２人目の素数さん
2012/04/16(月) 21:01:05.39本当は図書館とかがもっと良いのだけど
0209１３２人目の素数さん
2012/04/16(月) 21:32:40.900210１３２人目の素数さん
2012/04/18(水) 21:07:49.08最小論理じゃ⊥→¬¬Aしか証明できないですよね・・・
0211１３２人目の素数さん
2012/04/19(木) 00:59:06.46JECHのSET THEORYのペーパーバック版の次の入荷8月だって。
まだまだ全然届かないよ。
COOPERのComputabilyty THOERYのほうも多分遅くなるんだろうけど。
0212１３２人目の素数さん
2012/04/20(金) 17:41:51.000213１３２人目の素数さん
2012/04/20(金) 18:27:54.08すいませんが今回の書き込みで何が伝えたいんでしょうか？
このスレッドは数理論理学に興味を持つ人々が集まって
一緒に話題を共有しようとして作られました。
今回の書き込みが
そういった人々に対して失礼にならないと保証できますか？
0214１３２人目の素数さん
2012/04/20(金) 19:14:12.750215１３２人目の素数さん
2012/04/20(金) 21:11:59.82任意の論理式ψが、古典論理において妥当式であり、
直観主義論理で証明不可能であることは、どのように
証明もしくは定義できるのでしょうか?
たとえば、任意の論理式ψの全ての演繹を定義できるので
あれば、それら演繹の中に証明であるものが存在しない事を
証明すればいいと思います。
しかし、古典論理において論理式ψが妥当式であれば、
論理式ψがたとえ有限であっても、背理法などを考えれば、
その演繹は無限に存在するように思います。
任意の論理式ψについて、直観主義論理の範囲で有効な演繹は
論理式ψが有限であれば、有限個しかないのでしょうか?
結局何が言いたいかと言うと、直観主義論理において
証明不可能であることを証明する自動証明アルゴリズムは
存在するのでしょうか？
0216１３２人目の素数さん
2012/04/20(金) 21:36:38.38命題論理の完全性から、ほぼ明らかだとは思うのですが・・・
古典論理において、有限長の全ての妥当式は有限回の
公理の使用によって証明できるのでしょうか?
最小論理に、2重否定の除去(¬¬A→A)を加えた論理は
古典論理と等しいことは自明です。
ならば、ψが古典論理において妥当式ならば、
(¬¬)*ψで示される論理式の何れかが、
最小論理で証明可能であると言えるのでしょうか?
((¬¬)*は、¬¬の0回以上の有限の繰り返し)
0217１３２人目の素数さん
2012/04/20(金) 21:36:56.99A ¬A
⊥
¬¬A
A→¬¬A
であることから、A→¬¬Aは、やはり最小論理で
証明できると思うので、
任意(有限長)の妥当式ψについて、(¬¬){k,}ψで
示される全ての論理式が、最小論理で証明できる
有限のkが常に存在すると言えるのでしょうか?
((¬¬){k,}は、¬¬のk回以上の繰り返し)
結局、なにが言いたいかと言うと、最小論理に
使用回数を限定した2重否定除去公理を加えた
論理はどのような性質を持つのでしょうか?
(当然、そこから導かれる定理を使用した場合も
使用回数を消費すると考えて)
少なくとも、古典論理に包含されることは明らかですが、
使用回数の定義の仕方によっては、古典論理より弱く
直観主義論理より強くしたり、直観主義論理より弱く、
古典論理より強くしたり出来るのでしょうか?
0218１３２人目の素数さん
2012/04/20(金) 21:48:28.06量化子を持つ論理体系は決定不能。
そのような自動証明アルゴリズムは存在しない。
0219１３２人目の素数さん
2012/04/20(金) 21:50:19.16したがってBであーる
0220218
2012/04/20(金) 21:51:34.580221１３２人目の素数さん
2012/04/20(金) 22:56:30.17, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0222１３２人目の素数さん
2012/04/20(金) 23:19:53.96(Ｐ⊃Ｑ)⊃(〜Ｑ⊃〜Ｐ)は恒真式で、「(ＰならばＱ)ならば(ＱでなけばＰではない)」が
成立するが、[Ｐ⊃(ＱＶＲ)]⊃[(Ｐ⊃Ｑ)Ｖ(Ｐ⊃Ｒ)] は恒真式なのに、
[Ｐならば(ＱかＲ)]ならば[(ＰならばＱ)か又は(ＰならばＲである)] は成立しない★
0223１３２人目の素数さん
2012/04/20(金) 23:35:18.51(Ｐ⊃Ｑ)⊃(〜Ｑ⊃〜Ｐ)ってことは
(P←Q)←(¬Q←¬P)
だぞ？
0224１３２人目の素数さん
2012/04/20(金) 23:37:56.51, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0225１３２人目の素数さん
2012/04/20(金) 23:40:12.24前の質問の言い直しじゃなくて別の質問が書いてある気がする
着眼点とかは面白いとは思うのだけど
まずは完全性定理とか、
古典論理を直観主義論理に埋め込む方法
（http://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation）
とかを勉強したらいいと思う
それから簡単なリマークとして、
直観主義論理でも¬¬¬φ→¬φは証明できるので
¬¬¬¬φは¬¬φと同値になります
0226１３２人目の素数さん
2012/04/21(土) 07:54:38.82, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0227１３２人目の素数さん
2012/04/21(土) 10:41:48.87とかには見られるが、最近はあまり採用されていないと思う。
これは、命題の意味を素朴に集合で考えたときに
「部分集合」と完全に逆方向になって誤解されやすいからでしょう。
つまり、「A ならば B」を
∀x(x∈A ならば x∈B)
と解釈（？）すると、これはまさに部分集合としは
A ⊂ B
という意味なので。
>> 223 も、このように読んだのですね。
0228１３２人目の素数さん
2012/04/21(土) 12:15:33.84[Ｐ⊃(ＱＶＲ)]⊃[(Ｐ⊃Ｑ)Ｖ(Ｐ⊃Ｒ)]
を
(P→(QＶR))→((P→Q)∨(P→R))
と解釈するなら、排中律を認めなければならないが、
認めないような考え方をしたり、前提を作ったりすると
そりゃ、成り立つとは言えないんじゃないだろうか?
たとえば、
(人間ならば、男か女である。)→
((人間ならば男である)または(人間ならば女である))
排中律を採用するならば、前提
人間ならば、男か女である。
が真であるか偽であるのどちらかである。
偽であれば、爆発原理から命題は真。
つまり、
人間ならば、男か女か┌（┌ ＾o＾）┐ﾎﾓｫ･･･である。
ならば、前提は偽となるため、爆発原理から命題は真。
直感に反するとすれば、この辺なのではないでしょうか?
0229１３２人目の素数さん
2012/04/21(土) 12:38:37.05(P→(QＶR))→((P→Q)∨(P→R))
について排中律あれば証明できる事は理解できるが、
排中律がなければ、証明できない事をどのように
証明できるのか？
と言うのが、私の疑問。
0230１３２人目の素数さん
2012/04/21(土) 12:58:23.10, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0231１３２人目の素数さん
2012/04/21(土) 16:59:53.65「人間ならば男かまたは女である」は命題論理じゃなくて述語論理の命題だよね。
∀x(P(x)→(Q(x)∨R(x)))の形でしょ
0232１３２人目の素数さん
2012/04/21(土) 17:38:54.06P,Q,Rが、どのような命題であっても論理式が真である
って意味ですよね。
P,Q,Rは任意の命題なのだから、
Pを「人間である。」と考え、
Qを「男である。」と考え、
Rを「女である。」と考え、
(人間ならば、男か女である。)→
((人間ならば男である)または(人間ならば女である))
は、(P→(QＶR))→((P→Q)∨(P→R))で表現される命題の
1つではないですか?
(人間ならば、男か女である。)→
((人間ならば男である)または(人間ならば女である))
0233１３２人目の素数さん
2012/04/21(土) 17:47:31.08Pを「犬である。」と考え、
Qを「人間である。」と考え、
Rを「女である。」と考え、
としても、排中律と爆発原理を認めるなら、
(犬ならば、人間か女である。)→
((犬ならば人間である)または(犬ならば女である))
は、真である。というのが妥当式だと私は理解しているのですが
違うのでしょうか？
0234１３２人目の素数さん
2012/04/21(土) 17:48:41.64, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0235１３２人目の素数さん
2012/04/21(土) 17:52:38.64「人間ならば、男か女である」は真か偽かのどちらかであるは、
(人間ならば、男か女である)∨¬(人間ならば、男か女である)
と言う意味でなので、上記主張は
∀x(P(x)→(Q(x)∨R(x)))
じゃないと思います。
0236１３２人目の素数さん
2012/04/21(土) 17:54:02.05, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0237１３２人目の素数さん
2012/04/21(土) 18:01:42.55, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0238１３２人目の素数さん
2012/04/21(土) 21:21:25.94諭されているのでしょうか・・・・
>>215
に関しては、結局以下が同値であることを証明すれば
良いのですよね。
1.論理式ψが古典論理で証明可能で、
直観主義論理で証明不可能。
2.論理式ψが古典論理で証明可能で、
直観主義論理に論理式ψを公理
として加えた論理で、排中律が
証明可能。
どちらにしても、>>225の仰るとおり、完全性定理と
古典論理を直観主義論理に埋め込む方法をもう少し
ちゃんと勉強すべきなんでしょう・・・。
0239１３２人目の素数さん
2012/04/21(土) 22:25:38.420240１３２人目の素数さん
2012/04/21(土) 22:53:38.041.論理式ψが古典論理で証明可能で、
直観主義論理で証明不可能。
2.論理式ψが古典論理で証明可能で、
直観主義論理に論理式ψを公理
として加えた論理で、排中律が
証明可能。
この２条件は同値ではありません。
反例：ψ = (p→q)∨(q→p)
(p→q)∨(q→p)を直観主義論理に公理として加えたら
直観主義論理と古典論理の間に位置する「中間論理」になります。
中間論理は他にもたくさんあります（非可算無限個あります）。
たとえば鹿島亮の数理論理学には中間論理や
「論理式（たとえば(p→q)∨(q→p)）が直観主義論理で証明不可能なこと」
をクリプケモデルを構成して示すことが載っているので、
その辺りを勉強するとよいのでは。
0241１３２人目の素数さん
2012/04/21(土) 23:18:11.461億人から選ばれた1人（A)が、1億人全員から口座に1円づつ振り込まれるとする
毎月1人選ばれるとすると1年間に12人が1億円の資産を持つことができる
10年で120人 20年で240人 30年で360人が1億円を手にできる
宝くじより確実
1億人全員が1億円持つことは可能か
0242１３２人目の素数さん
2012/04/21(土) 23:22:08.94クリプキ・クリプケどっちが標準的なんだろう？
0243１３２人目の素数さん
2012/04/21(土) 23:22:35.40全員がものすごく長寿ならほぼ可能。
0244１３２人目の素数さん
2012/04/21(土) 23:27:11.61世界番号付きのタブロー法とかで証明可能か簡単に分かるよ。
0245１３２人目の素数さん
2012/04/21(土) 23:57:36.12, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
0246１３２人目の素数さん
2012/04/22(日) 06:50:01.43>>244
ありがとう。要は認識論理の勉強をすればいいのですね。
0247１３２人目の素数さん
2012/04/22(日) 07:01:19.18そもそも、一番初めに全員の総資産が、(1億)^2円なければ、
1億人全員が1億円持つことは不可能じゃ？
・・・そういうことじゃないの？
0248１３２人目の素数さん
2012/04/22(日) 08:32:13.06http://www.amazon.com/Introduction-Non-Classical-Logic-Introductions-Philosophy/dp/0521670268
この本に非古典論理のタブロー法のやり方が色々載ってる
0249240
2012/04/22(日) 09:53:10.60どういたしまして。
しかしあなたは、私(240)も244も認識論理なんていう単語を
まったく発していないのに、なぜこんなことを言うのですか？
0250１３２人目の素数さん
2012/04/22(日) 10:04:43.28ググった結果、
クリプキモデル 約 11,200 件
クリプケモデル 約 427 件
でクリプキモデルの勝ち。
0251１３２人目の素数さん
2012/04/22(日) 10:59:59.82結構大きいことをおっしゃる人でしたが。
0252１３２人目の素数さん
2012/04/22(日) 11:00:53.59, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
■ このスレッドは過去ログ倉庫に格納されています