数理論理学（数学基礎論） その11
レス数が1000を超えています。これ以上書き込みはできません。
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化
などを参照）
前スレ
数学基礎論・数理論理学 その10
http://uni.2ch.net/test/read.cgi/math/1319895756/ >>912
その具体例…論理式を表す記号列の解釈が一意に確定すること…に関する議論は｢論理学を作る」の前半部分で議論されていた記憶がうっすらとあります >>943
外延記法や和集合の記号を追加していったとき、
集合一般に関して左端に∈が現れないことを示すには、論理式の長さもしくは論理式の構成に関する帰納法が必要
そこまで一般的な主張をせず、「∈ ＋ 変数記号」が集合でないことを示すだけに留めるとしても、
>>912と同様に文字数に関する考察が必要 有限の長さを持つ任意の文字列というものを考えるとき
a_1 a_2 …… a_n
を頭に思い浮かべることと思うが、
……で省略された部分があるにも関わらず、直感的に有限列の性質を把握することができる
それ以前に有限の長さが何を意味するかも何故か知っている
メタレベルにおけるこの得体の知れない直感を（論理法則と同様に）そのままの形で受け入れるか、
自然数の性質に起因するものであると見なすか
どちらか選ぶとすれば俺なら後者だね >>876
そりゃそうですね。証明されない論理式見つけるのに、最初はゲーデル文
見つけるくらい大変だったんですからね。でも直観主義者って、B∨¬B
の形の論理式を公理にしてはいけないって言うんだから、つまりは
B∨¬Bの形の論理式でも正しいとはいえない論理式があると信じている
んですよね。というわりには、じゃあそういう形の（述語論理の）論理式
を見せてみろっていうと、見せれないんですよね。直観主義者の人って存在
すると言ったら実際に見せることができないと気がすまない人たちなんじゃ
あなかったのかなあ。 >>958
Bが原始論理式のとき直観主義論理でB∨¬Bが証明可能でないことが
カット除去定理よりただちに分かる >>958
直観主義においてB∨¬Bとは、Bまたは¬Bが証明できる、ということを意味します
もし仮に、B∨¬Bという論理式が証明可能だとすると、Bもしくは¬Bが証明可能ということになり、公理系にBや¬Bが入っている(もしくは定理として導ける)ことを意味します
ですから、任意の論理式やその否定が前提としてない限り、B∨¬Bは証明することができない、ということです >>960
直観主義者じゃないかもだけど
公理化至上主義者かもな
いずれにせよ絶滅危惧種だ >>961
「Bが証明できるかまたは¬Bが証明できる」という意味だとすると、
通常論理における（B∨¬B）に相当する概念はどう書くの？ >>965
「B∨¬Bが証明できる｣ということが「Bが証明できる」または「¬Bが証明できる」という意味
なお
ここで言う｢証明できる｣は｢形式的に証明できる｣ということね >>976
それは「直観主義における（B∨¬B）」の意味でしょ。
そうじゃなくて、
「通常論理における（B∨¬B）」
に相当する概念はどう書くのかを聞いてる。
∨ を使ったらダメなんでしょ？ >>979
>それは「直観主義における（B∨¬B）」の意味でしょ。
違うよ
直観主義における「B∨¬Bが証明できる」の意味だよ
B∨¬Bの意味は「BまたはBでない」でいいけど
真偽の2値で考えることができないというだけ
3値論理だと
Bが真または偽ならB∨¬Bは真だけど
Bが第3の論理値ならB∨¬Bは第3の論理値 >>959
例えばPAの公理からはじめて、排中律を使わなくても(1=3∨¬1=3)は簡単に証明
できますよ。
>>961
だから、証明できない論理式があるなら具体的に教えてほしかったんです。
そうすれば、例えば
「PAの公理からはじめて、排中律を使わない場合に
B∨¬B(具体的な形)は証明できません
当然¬(B∨¬B)も証明できません
ということで、直観主義論理にこだわるなら証明も反証もできない論理式
が簡単に見つかるんだ。」
と結論したかったんです。
でもここのレス>>876のおかげで、結局はそう簡単にはいかなさそうだとわかりました。 B∨¬B自体が証明できない論理式そのものなんですよ
具体的な論理式とかではなく、B∨¬B自体が対象としての論理式なのです
Bはワイルドカードとしても捉えることができますが、対象としての原子論理式たる命題そのものとも捉えられます 直観主義では|-B∨¬Bを示すことはできません
B|-B∨¬Bや¬B|-B∨¬Bは示せます B∨¬Bがあなたの知りたい具体的な論理式だということです ＞証明できない論理式
古典論理でもＡは証明できないよ >>997
そこは古典論理で証明できて直観論理で証明できないと意訳すべし 直観論理で
B∨¬B
は証明できないけど
¬(B∧¬B)
は証明できるのよね >>999
直観主義論理に於いては、∧と∨と、あるいは∀と∃とはもはや双対ではなく
従ってド・モルガンの法則は成り立たないから
なお一言注意しておくと、「直観論理」という言葉は存在しない
正しくは「直観主義論理」です
英語だと“intuitionistic（“intuitionism”の形容詞形で“-ism”なので「−主義」） logic”であって
“intuitive（“intuition”：「直観」の形容詞形） logic”じゃないからです このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 2134日 3時間 34分 0秒 5ちゃんねるの運営はプレミアム会員の皆さまに支えられています。
運営にご協力お願いいたします。
───────────────────
《プレミアム会員の主な特典》
★ 5ちゃんねる専用ブラウザからの広告除去
★ 5ちゃんねるの過去ログを取得
★ 書き込み規制の緩和
───────────────────
会員登録には個人情報は一切必要ありません。
月300円から匿名でご購入いただけます。
▼ プレミアム会員登録はこちら ▼
https://premium.5ch.net/
▼ 浪人ログインはこちら ▼
https://login.5ch.net/login.php レス数が1000を超えています。これ以上書き込みはできません。
