数理論理学（数学基礎論）　その11

1 ：１３２人目の素数さん：2011/12/30(金) 21:17:20.12 .net

数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
　若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化
などを参照）

前スレ
数学基礎論・数理論理学　その10
http://uni.2ch.net/test/read.cgi/math/1319895756/

953 ：￥ ：2017/11/01(水) 12:21:29.62 ID:cSPyhj3J.net

￥

954 ：￥ ：2017/11/01(水) 12:21:46.97 ID:cSPyhj3J.net

￥

955 ：￥ ：2017/11/01(水) 12:22:07.06 ID:cSPyhj3J.net

￥

956 ：１３２人目の素数さん：2017/11/01(水) 12:40:50.74 .net

>>913
その具体例…論理式を表す記号列の解釈が一意に確定すること…に関する議論は｢論理学を作る」の前半部分で議論されていた記憶がうっすらとあります

957 ：１３２人目の素数さん：2017/11/01(水) 13:11:13.35 ID:ScFh/IWE.net

>>944
外延記法や和集合の記号を追加していったとき、
集合一般に関して左端に∈が現れないことを示すには、論理式の長さもしくは論理式の構成に関する帰納法が必要
そこまで一般的な主張をせず、「∈　＋　変数記号」が集合でないことを示すだけに留めるとしても、
>>913と同様に文字数に関する考察が必要

958 ：１３２人目の素数さん：2017/11/01(水) 13:26:11.98 ID:ScFh/IWE.net

有限の長さを持つ任意の文字列というものを考えるとき
a_1 a_2 …… a_n
を頭に思い浮かべることと思うが、
……で省略された部分があるにも関わらず、直感的に有限列の性質を把握することができる
それ以前に有限の長さが何を意味するかも何故か知っている

メタレベルにおけるこの得体の知れない直感を（論理法則と同様に）そのままの形で受け入れるか、
自然数の性質に起因するものであると見なすか
どちらか選ぶとすれば俺なら後者だね

959 ：867：2017/11/01(水) 14:46:49.14 ID:iHEq1qM3.net

>>877
そりゃそうですね。証明されない論理式見つけるのに、最初はゲーデル文
見つけるくらい大変だったんですからね。でも直観主義者って、B∨¬B
の形の論理式を公理にしてはいけないって言うんだから、つまりは
B∨¬Bの形の論理式でも正しいとはいえない論理式があると信じている
んですよね。というわりには、じゃあそういう形の（述語論理の）論理式
を見せてみろっていうと、見せれないんですよね。直観主義者の人って存在
すると言ったら実際に見せることができないと気がすまない人たちなんじゃ
あなかったのかなあ。

960 ：１３２人目の素数さん：2017/11/01(水) 14:59:08.89 ID:ScFh/IWE.net

>>959
Bが原始論理式のとき直観主義論理でB∨¬Bが証明可能でないことが
カット除去定理よりただちに分かる

961 ：１３２人目の素数さん：2017/11/01(水) 17:59:08.10 ID:DNDHRFTY.net

直感主義者は板から出てけ　うざい

962 ：１３２人目の素数さん：2017/11/01(水) 18:04:29.61 ID:cyvcTwxs.net

>>959
直観主義においてB∨¬Bとは、Bまたは¬Bが証明できる、ということを意味します

もし仮に、B∨¬Bという論理式が証明可能だとすると、Bもしくは¬Bが証明可能ということになり、公理系にBや¬Bが入っている(もしくは定理として導ける)ことを意味します

ですから、任意の論理式やその否定が前提としてない限り、B∨¬Bは証明することができない、ということです

963 ：１３２人目の素数さん：2017/11/01(水) 18:21:48.91 ID:Gr+Xy0/3.net

>>957
うんにゃ
全然要らない

964 ：１３２人目の素数さん：2017/11/01(水) 18:24:08.30 ID:Gr+Xy0/3.net

>>961
直観主義者じゃないかもだけど
公理化至上主義者かもな
いずれにせよ絶滅危惧種だ

965 ：１３２人目の素数さん：2017/11/01(水) 18:43:11.16 ID:ScFh/IWE.net

>>964
「直感主義者」って君のことだろ

966 ：１３２人目の素数さん：2017/11/01(水) 19:38:07.96 ID:VCwpMl0X.net

>>962
「Bが証明できるかまたは¬Bが証明できる」という意味だとすると、
通常論理における（B∨¬B）に相当する概念はどう書くの？

967 ：￥ ：2017/11/01(水) 22:30:03.84 ID:cSPyhj3J.net

￥

968 ：￥ ：2017/11/01(水) 22:30:25.59 ID:cSPyhj3J.net

￥

969 ：￥ ：2017/11/01(水) 22:30:41.92 ID:cSPyhj3J.net

￥

970 ：￥ ：2017/11/01(水) 22:30:59.68 ID:cSPyhj3J.net

￥

971 ：￥ ：2017/11/01(水) 22:31:20.50 ID:cSPyhj3J.net

￥

972 ：￥ ：2017/11/01(水) 22:31:38.07 ID:cSPyhj3J.net

￥

973 ：￥ ：2017/11/01(水) 22:31:56.75 ID:cSPyhj3J.net

￥

974 ：￥ ：2017/11/01(水) 22:32:14.65 ID:cSPyhj3J.net

￥

975 ：￥ ：2017/11/01(水) 22:32:34.27 ID:cSPyhj3J.net

￥

976 ：￥ ：2017/11/01(水) 22:32:55.29 ID:cSPyhj3J.net

￥

977 ：１３２人目の素数さん：2017/11/02(木) 00:18:11.28 ID:kb3Y9mL5.net

>>966
「B∨¬Bが証明できる｣ということが「Bが証明できる」または「¬Bが証明できる」という意味
なお
ここで言う｢証明できる｣は｢形式的に証明できる｣ということね

978 ：１３２人目の素数さん：2017/11/02(木) 00:18:36.64 ID:kb3Y9mL5.net

>>965
ぷ

979 ：１３２人目の素数さん：2017/11/02(木) 00:22:36.54 ID:Rv2iV+x2.net

>>977
無理して回答しようとしなくていいよｗ

980 ：１３２人目の素数さん：2017/11/02(木) 00:30:24.24 ID:t3jIOnxn.net

>>977
それは「直観主義における（B∨¬B）」の意味でしょ。

そうじゃなくて、
「通常論理における（B∨¬B）」
に相当する概念はどう書くのかを聞いてる。
∨　を使ったらダメなんでしょ？

981 ：￥ ：2017/11/02(木) 01:13:25.79 ID:23MnTxXU.net

￥

982 ：￥ ：2017/11/02(木) 01:13:47.56 ID:23MnTxXU.net

￥

983 ：￥ ：2017/11/02(木) 01:14:05.64 ID:23MnTxXU.net

￥

984 ：￥ ：2017/11/02(木) 01:14:23.78 ID:23MnTxXU.net

￥

985 ：￥ ：2017/11/02(木) 01:14:39.44 ID:23MnTxXU.net

￥

986 ：￥ ：2017/11/02(木) 01:14:57.19 ID:23MnTxXU.net

￥

987 ：￥ ：2017/11/02(木) 01:15:19.42 ID:23MnTxXU.net

￥

988 ：￥ ：2017/11/02(木) 01:15:40.15 ID:23MnTxXU.net

￥

989 ：￥ ：2017/11/02(木) 01:16:00.30 ID:23MnTxXU.net

￥

990 ：￥ ：2017/11/02(木) 01:16:18.48 ID:23MnTxXU.net

￥

991 ：１３２人目の素数さん：2017/11/02(木) 07:13:12.80 ID:kb3Y9mL5.net

>>980
>それは「直観主義における（B∨¬B）」の意味でしょ。
違うよ
直観主義における「B∨¬Bが証明できる」の意味だよ
B∨¬Bの意味は「BまたはBでない」でいいけど
真偽の2値で考えることができないというだけ
3値論理だと
Bが真または偽ならB∨¬Bは真だけど
Bが第3の論理値ならB∨¬Bは第3の論理値

992 ：１３２人目の素数さん：2017/11/02(木) 09:01:11.76 ID:/fC06Pyx.net

ん

993 ：１３２人目の素数さん：2017/11/02(木) 14:56:03.91 .net

直近50レスの流れ的に、学部生ですかな？

994 ：867：2017/11/02(木) 15:03:26.03 ID:j55Wc5r5.net

>>960
例えばPAの公理からはじめて、排中律を使わなくても(1=3∨¬1=3)は簡単に証明
できますよ。

>>962
だから、証明できない論理式があるなら具体的に教えてほしかったんです。
そうすれば、例えば

「PAの公理からはじめて、排中律を使わない場合に
　B∨¬B(具体的な形)は証明できません
　当然¬(B∨¬B)も証明できません
ということで、直観主義論理にこだわるなら証明も反証もできない論理式
が簡単に見つかるんだ。」

と結論したかったんです。
でもここのレス>>877のおかげで、結局はそう簡単にはいかなさそうだとわかりました。

995 ：１３２人目の素数さん：2017/11/02(木) 15:13:50.39 ID:CxkP7QYO.net

B∨¬B自体が証明できない論理式そのものなんですよ
具体的な論理式とかではなく、B∨¬B自体が対象としての論理式なのです
Bはワイルドカードとしても捉えることができますが、対象としての原子論理式たる命題そのものとも捉えられます

996 ：１３２人目の素数さん：2017/11/02(木) 15:18:02.58 ID:CxkP7QYO.net

直観主義では|-B∨¬Bを示すことはできません
B|-B∨¬Bや¬B|-B∨¬Bは示せます

997 ：１３２人目の素数さん：2017/11/02(木) 15:21:34.83 ID:CxkP7QYO.net

B∨¬Bがあなたの知りたい具体的な論理式だということです

998 ：１３２人目の素数さん：2017/11/02(木) 19:38:28.78 ID:gkHUdXs2.net

＞証明できない論理式

古典論理でもＡは証明できないよ

999 ：１３２人目の素数さん：2017/11/02(木) 20:24:16.56 ID:kb3Y9mL5.net

>>998
そこは古典論理で証明できて直観論理で証明できないと意訳すべし

1000 ：１３２人目の素数さん：2017/11/02(木) 20:25:09.93 ID:kb3Y9mL5.net

直観論理で
B∨¬B
は証明できないけど
¬(B∧¬B)
は証明できるのよね

1001 ：１３２人目の素数さん：2017/11/03(金) 00:51:20.59 ID:i9930jhu.net

>>1000
直観主義論理に於いては、∧と∨と、あるいは∀と∃とはもはや双対ではなく
従ってド・モルガンの法則は成り立たないから

なお一言注意しておくと、「直観論理」という言葉は存在しない
正しくは「直観主義論理」です

英語だと“intuitionistic（“intuitionism”の形容詞形で“-ism”なので「−主義」） logic”であって
“intuitive（“intuition”：「直観」の形容詞形） logic”じゃないからです

1002 ：2ch.net投稿限界：Over 1000 Thread

2ch.netからのレス数が1000に到達しました。