17/11/01 08:16:22.77 ScFh/IWE.net
>>932
その場合、集合の左端に∈が現れないことを（数学的帰納法で）示しておかないと駄目
981:１３２人目の素数さん
17/11/01 11:16:42.38 uNaz/Y1J.net
>>943
不要
982:１３２人目の素数さん
17/11/01 11:17:29.96 uNaz/Y1J.net
特に数学的帰納法は不要
983:￥
17/11/01 12:19:28.72 cSPyhj3J.net
￥
984:￥
17/11/01 12:19:50.95 cSPyhj3J.net
￥
985:￥
17/11/01 12:20:07.93 cSPyhj3J.net
￥
986:￥
17/11/01 12:20:23.67 cSPyhj3J.net
￥
987:￥
17/11/01 12:20:39.23 cSPyhj3J.net
￥
988:￥
17/11/01 12:20:56.05 cSPyhj3J.net
￥
989:￥
17/11/01 12:21:13.16 cSPyhj3J.net
￥
990:￥
17/11/01 12:21:29.62 cSPyhj3J.net
￥
991:￥
17/11/01 12:21:46.97 cSPyhj3J.net
￥
992:￥
17/11/01 12:22:07.06 cSPyhj3J.net
￥
993:１３２人目の素数さん
17/11/01 12:40:50.74 .net
>>913
その具体例…論理式を表す記号列の解釈が一意に確定すること…に関する議論は｢論理学を作る」の前半部分で議論されていた記憶がうっすらとあります
994:１３２人目の素数さん
17/11/01 13:11:13.35 ScFh/IWE.net
>>944
外延記法や和集合の記号を追加していったとき、
集合一般に関して左端に∈が現れないことを示すには、論理式の長さもしくは論理式の構成に関する帰納法が必要
そこまで一般的な主張をせず、「∈ ＋ 変数記号」が集合でないことを示すだけに留めるとしても、
>>913と同様に文字数に関する考察が必要
995:１３２人目の素数さん
17/11/01 13:26:11.98 ScFh/IWE.net
有限の長さを持つ任意の文字列というものを考えるとき
a_1 a_2 …… a_n
を頭に思い浮かべることと思うが、
……で省略された部分があるにも関わらず、直感的に有限列の性質を把握することができる
それ以前に有限の長さが何を意味するかも何故か知っている
メタレベルにおけるこの得体の知れない直感を（論理法則と同様に）そのままの形で受け入れるか、
自然数の性質に起因するものであると見なすか
どちらか選ぶとすれば俺なら後者だね
996:867
17/11/01 14:46:49.14 iHEq1qM3.net
>>877
そりゃそうですね。証明されない論理式見つけるのに、最初はゲーデル文
見つけるくらい大変だったんですからね。でも直観主義者って、B∨￢B
の形の論理式を公理にしてはいけないって言うんだから、つまりは
B∨￢Bの形の論理式でも正しいとはいえない論理式があると信じている
んですよね。というわりには、じゃあそういう形の（述語論理の）論理式
を見せてみろっていうと、見せれないんですよね。直観主義者の人って存在
すると言ったら実際に見せることができないと気がすまない人たちなんじゃ
あなかったのかなあ。
997:１３２人目の素数さん
17/11/01 14:59:08.89 ScFh/IWE.net
>>959
Bが原始論理式のとき直観主義論理でB∨￢Bが証明可能でないことが
カット除去定理よりただちに分かる
998:１３２人目の素数さん
17/11/01 17:59:08.10 DNDHRFTY.net
直感主義者は板から出てけ うざい
999:１３２人目の素数さん
17/11/01 18:04:29.61 cyvcTwxs.net
>>959
直観主義においてB∨¬Bとは、Bまたは¬Bが証明できる、ということを意味します
もし仮に、B∨¬Bという論理式が証明可能だとすると、Bもしくは¬Bが証明可能ということになり、公理系にBや¬Bが入っている(もしくは定理として導ける)ことを意味します
ですから、任意の論理式やその否定が前提としてない限り、B∨¬Bは証明することができない、ということです
1000:１３２人目の素数さん
17/11/01 18:21:48.91 Gr+Xy0/3.net
>>957
うんにゃ
全然要らない
1001:１３２人目の素数さん
17/11/01 18:24:08.30 Gr+Xy0/3.net
>>961
直観主義者じゃないかもだけど
公理化至上主義者かもな
いずれにせよ絶滅危惧種だ
1002:１３２人目の素数さん
17/11/01 18:43:11.16 ScFh/IWE.net
>>964
「直感主義者」って君のことだろ
1003:１３２人目の素数さん
17/11/01 19:38:07.96 VCwpMl0X.net
>>962
「Bが証明できるかまたは¬Bが証明できる」という意味だとすると、
通常論理における（B∨¬B）に相当する概念はどう書くの？
1004:￥
17/11/01 22:30:03.84 cSPyhj3J.net
￥
1005:￥
17/11/01 22:30:25.59 cSPyhj3J.net
￥
1006:￥
17/11/01 22:30:41.92 cSPyhj3J.net
￥
1007:￥
17/11/01 22:30:59.68 cSPyhj3J.net
￥
1008:￥
17/11/01 22:31:20.50 cSPyhj3J.net
￥
1009:￥
17/11/01 22:31:38.07 cSPyhj3J.net
￥
1010:￥
17/11/01 22:31:56.75 cSPyhj3J.net
￥
1011:￥
17/11/01 22:32:14.65 cSPyhj3J.net
￥
1012:￥
17/11/01 22:32:34.27 cSPyhj3J.net
￥
1013:￥
17/11/01 22:32:55.29 cSPyhj3J.net
￥
1014:１３２人目の素数さん
17/11/02 00:18:11.28 kb3Y9mL5.net
>>966
「B∨￢Bが証明できる｣ということが「Bが証明できる」または「￢Bが証明できる」という意味
なお
ここで言う｢証明できる｣は｢形式的に証明できる｣ということね
1015:１３２人目の素数さん
17/11/02 00:18:36.64 kb3Y9mL5.net
>>965
ぷ
1016:１３２人目の素数さん
17/11/02 00:22:36.54 Rv2iV+x2.net
>>977
無理して回答しようとしなくていいよｗ
1017:１３２人目の素数さん
17/11/02 00:30:24.24 t3jIOnxn.net
>>977
それは「直観主義における（B∨￢B）」の意味でしょ。
そうじゃなくて、
「通常論理における（B∨￢B）」
に相当する概念はどう書くのかを聞いてる。
∨ を使ったらダメなんでしょ？
1018:￥
17/11/02 01:13:25.79 23MnTxXU.net
￥
1019:￥
17/11/02 01:13:47.56 23MnTxXU.net
￥
1020:￥
17/11/02 01:14:05.64 23MnTxXU.net
￥
1021:￥
17/11/02 01:14:23.78 23MnTxXU.net
￥
1022:￥
17/11/02 01:14:39.44 23MnTxXU.net
￥
1023:￥
17/11/02 01:14:57.19 23MnTxXU.net
￥
1024:￥
17/11/02 01:15:19.42 23MnTxXU.net
￥
1025:￥
17/11/02 01:15:40.15 23MnTxXU.net
￥
1026:￥
17/11/02 01:16:00.30 23MnTxXU.net
￥
1027:￥
17/11/02 01:16:18.48 23MnTxXU.net
￥
1028:１３２人目の素数さん
17/11/02 07:13:12.80 kb3Y9mL5.net
>>980
>それは「直観主義における（B∨￢B）」の意味でしょ。
違うよ
直観主義における「B∨￢Bが証明できる」の意味だよ
B∨￢Bの意味は「BまたはBでない」でいいけど
真偽の2値で考えることができないというだけ
3値論理だと
Bが真または偽ならB∨￢Bは真だけど
Bが第3の論理値ならB∨￢Bは第3の論理値
1029:１３２人目の素数さん
17/11/02 09:01:11.76 /fC06Pyx.net
ん
1030:１３２人目の素数さん
17/11/02 14:56:03.91 .net
直近50レスの流れ的に、学部生ですかな？
1031:867
17/11/02 15:03:26.03 j55Wc5r5.net
>>960
例えばPAの公理からはじめて、排中律を使わなくても(1=3∨￢1=3)は簡単に証明
できますよ。
>>962
だから、証明できない論理式があるなら具体的に教えてほしかったんです。
そうすれば、例えば
「PAの公理からはじめて、排中律を使わない場合に
B∨￢B(具体的な形)は証明できません
当然￢(B∨￢B)も証明できません
ということで、直観主義論理にこだわるなら証明も反証もできない論理式
が簡単に見つかるんだ。」
と結論したかったんです。
でもここのレス>>877のおかげで、結局はそう簡単にはいかなさそうだとわかりました。
1032:１３２人目の素数さん
17/11/02 15:13:50.39 CxkP7QYO.net
B∨¬B自体が証明できない論理式そのものなんですよ
具体的な論理式とかではなく、B∨¬B自体が対象としての論理式なのです
Bはワイルドカードとしても捉えることができますが、対象としての原子論理式たる命題そのものとも捉えられます
1033:１３２人目の素数さん
17/11/02 15:18:02.58 CxkP7QYO.net
直観主義では|-B∨¬Bを示すことはできません
B|-B∨¬Bや¬B|-B∨¬Bは示せます
1034:１３２人目の素数さん
17/11/02 15:21:34.83 CxkP7QYO.net
B∨¬Bがあなたの知りたい具体的な論理式だということです
1035:１３２人目の素数さん
17/11/02 19:38:28.78 gkHUdXs2.net
＞証明できない論理式
古典論理でもＡは証明できないよ
1036:１３２人目の素数さん
17/11/02 20:24:16.56 kb3Y9mL5.net
>>998
そこは古典論理で証明できて直観論理で証明できないと意訳すべし
1037:１３２人目の素数さん
17/11/02 20:25:09.93 kb3Y9mL5.net
直観論理で
B∨￢B
は証明できないけど
￢(B∧￢B)
は証明できるのよね
1038:１３２人目の素数さん
17/11/03 00:51:20.59 i9930jhu.net
>>1000
直観主義論理に於いては、∧と�
1039:ﾉと、あるいは∀と∃とはもはや双対ではなく 従ってド・モルガンの法則は成り立たないから なお一言注意しておくと、「直観論理」という言葉は存在しない 正しくは「直観主義論理」です 英語だと“intuitionistic（“intuitionism”の形容詞形で“-ism”なので「－主義」） logic”であって “intuitive（“intuition”：「直観」の形容詞形） logic”じゃないからです
1040:1001
Over 1000 Thread.net
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 2134日 3時間 34分 0秒
1041:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています