12/01/07 08:38:42.87
>>137
少なくとも書かれている規則からだけでは無理。
何故なら ∀ｘA という形の論理式を問答無用で偽と解釈する
（それ以外は通常の解釈をする）意味論を考えると、
それら規則はすべて真であることを保存するが、
証明しようとしているのは真を保存しない。
何か忘れている規則があるはず。
144:１３２人目の素数さん
12/01/07 09:05:13.62
>>137
全称化は向きが逆だろ。
「A→BからA→∀ｘBが出る（ただしｘはAに自由に現れない）」
T|-AならT|-￢∀ｘA→A
全称化よりT|-￢∀ｘA→∀ｘA
よってT|-∀ｘA
145:１３２人目の素数さん
12/01/07 09:48:30.24
>>143
すみません、「A→BからA→∀ｘ」の間違いでした。
>>144
>T|-AならT|-￢∀ｘA→A
この部分と
>よってT|-∀ｘA
この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？
146:１３２人目の素数さん
12/01/07 16:33:08.81
本スレッド>>1の
「数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ」
は全くの誤りとして論破されました。
本スレッドは反数学的トンデモスレッドとして閉鎖されますので
以下のスレッドに移動願います。
数理論理学（数学基礎論） その11
ｽﾚﾘﾝｸ(math板)
147:１３２人目の素数さん
12/01/07 16:54:44.05
隔離スレから出てきちゃダメでしょ
148:１３２人目の素数さん
12/01/07 17:33:30.28
このスレ自身が数学板の中では 哲ヲタやキチガイ専用の隔離スレだったりしてな
149:１３２人目の素数さん
12/01/07 20:06:39.51
劣等感をはき散らすのはみっともない。
150:１３２人目の素数さん
12/01/07 20:08:39.18
>>148
わかっていても言っちゃいけないことがある
151:１３２人目の素数さん
12/01/07 20:13:00.92
>>150
大学の教員はそれをやる非常識人が多いんだよ。
そんな連中が学生相手に社会人としての常識を説いたりするから笑える。
152:１３２人目の素数さん
12/01/07 20:32:52.31
>>141のレス見て発狂したんだろ。
153:１３２人目の素数さん
12/01/07 20:58:34.99
閉鎖されますので、って閉鎖する権限持っているの？
こういう妄想してしまうのは、やっぱり人格障害なんだろうな。
154:１３２人目の素数さん
12/01/07 21:11:03.25
>>153
何をいまさらｗｗｗ
155:スレタイスレ446
12/01/07 22:20:46.89
>>139
＞そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？
掲示板を読んでいる人間が、隣に座って同じ本を一緒に読んでいる様を想像して書きます。
また、投稿欄に書いた文章を決して読み返さないこと。
（レス数を減らしてじっくり書き込む時間をとるのがベストなのかもしれない。）
＞前スレの「考える人」と同じ臭いを感じる。
確かに文体が似ていますね。
考える人（＝考えない人）というコテハンは、このスレのその5辺りから時折出没していますよ。
>>140
以後、レスの数は減らします。
156:１３２人目の素数さん
12/01/07 23:18:50.20
>>155
本を読んだけど理解できない人に解説するつもりで書いていて、
まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。
157:１３２人目の素数さん
12/01/07 23:46:45.99
>>156
お前さんも文章を推敲した方がいい
158:横
12/01/07 23:49:02.64
>>156
> 156 名前：１３２人目の素数さん [sage]： 2012/01/07(土) 23:18:50.20
> >>155
あなたは
> 本を読んだけど理解できない人に解説するつもりで書いていて、
> まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
と私は思います。
あなたは、わたしが
> その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。
159:１３２人目の素数さん
12/01/08 02:20:00.10
>>153
削除依頼が通ると思っているんだろ。
503 ：数学板住人：2012/01/03(火) 08:04:24.00 HOST:36-2-122-83.saitama.ap.gmo-isp.jp<8080><3128><8000><1080>[36.2.122.83]
削除対象アドレス：
ｽﾚﾘﾝｸ(math板)
削除理由・詳細・その他：
数理論理学（数学基礎論） その11
ｽﾚﾘﾝｸ(math板)
と重複しているため削除願います。
ちなみに同じく埼玉のマツシンと思われる人物が
498 ：数理論理学者：2011/10/30(日) 09:40:31.00 HOST:d180.GsaitamaFL22.vectant.ne.jp<8080><3128><8000><1080>[116.91.89.180]
削除対象アドレス：
ｽﾚﾘﾝｸ(math板)
削除理由・詳細・その他：
スレッドのタイトルについて審議中、
合意案を無視して勝手に立てられた為。
タイトル審議スレ
数学基礎論スレのスレタイを決めるスレ
ｽﾚﾘﾝｸ(math板)
という削除依頼も出している。
自分で削除を依頼したスレの次スレを自称するのに勤しんでいるという矛盾に
本人は気づいていないようだな。
160:１３２人目の素数さん
12/01/08 04:37:01.40
２ちゃんのテンプレの"間違い"を正すより、
スタンフォード哲学事典(SEP)の"間違い"を正すほうが
よっぽど価値があることなんではないのか、マツシンよ。
SEPに特攻した武勇伝を期待しているよ。
161:１３２人目の素数さん
12/01/08 06:09:56.90
>>148は、>>67に反論できなくなって、捨て台詞ってこと？
気の利いたことが言えなくなった奴って痛々しいな。
162:１３２人目の素数さん
12/01/08 07:39:28.89
そうだな、ここのスレの間違いが訂正されてもここの住人くらいにしか恩恵はない。
スタンフォードの事典の誤りが訂正されたら、世界中に恩恵がある。
あの記事の誤りを訂正させたら世界中から賞賛の嵐だぜ、マツシンよ。
こんなスレのテンプレなんて下らんことにこだわらないで、世界に羽ばたこうぜ、世界のマツシン！
163:１３２人目の素数さん
12/01/08 08:26:44.00
マツシンあるいはアスペと呼ばれている人は、本気であんなこと言っているの？それともネタ？
基礎論の最初の目的（の一つ）がパラドックスの解決だったかということと、
基礎論の研究の結果実際にパラドックスを解決できたかという、
全く別の問題（一方は歴史の問題、もう一方は数学または哲学の問題）を混同していて、
自分でそれに気づかないって普通の感覚では理解不能なんですが。
やっぱりネタで言っているんではないのかと。
164:１３２人目の素数さん
12/01/08 08:41:00.87
ネタだと思ってるんなら、火傷しないようにスルーしとけ。
奴には関わらんでいた方が幸せ。
と、何度か奴と関わったことのある俺がいっとく。
165:１３２人目の素数さん
12/01/08 09:47:16.07
そのマツシンって奴、素人が！素人が！って言ってるけど、
自分はどんな論文出版しているんだ？誰かデータ持ってないかな？
区体論の人と同じく、自分も素人なのに虚勢張って言っているだけか？
166:１３２人目の素数さん
12/01/08 09:57:35.73
>>127
C^{(n)}-基数というのは、一種類の基数ではないようだよ。
可測、超強、超コンパクト、膨大、超膨大等々、
様々な巨大基数公理のC^{(n)}-版が考えられるということらしい。
167:１３２人目の素数さん
12/01/08 18:21:24.54
>>145
>>T|-AならT|-￢∀ｘA→A
>この部分と
T|-AならT∪{￢∀ｘA}|-Aで、演繹定理より。
>>よってT|-∀ｘA
>この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？
排中律より∀ｘA∨￢∀ｘAだが、￢∀ｘAから∀ｘAがでるので、
どちらにしても∀ｘA。
168:１３２人目の素数さん
12/01/08 18:35:31.85
質問です。基礎論の大学院生は博士号取得までにいくつくらい論文を書くのが普通ですか？
169:１３２人目の素数さん
12/01/08 18:38:20.46
頭の悪そうな質問だな．
170:１３２人目の素数さん
12/01/08 18:49:00.93
数理論理学・数学基礎論というのが、もはや一つの分野とは言いがたくて、複数の分野の総称という感じ。
だから基礎論では一概にはいえなくて、分野ごとに論文の書きやすさは大きく異なる。
よく言われるのは、非古典論理や計算機科学寄りだと論文数が多くなる。
171:１３２人目の素数さん
12/01/08 19:11:56.59
>>155
また面白い話題を提供してくれることを期待しています。
172:１３２人目の素数さん
12/01/08 19:32:49.90
446氏が哲学板の論理学スレに出現してる
173:１３２人目の素数さん
12/01/08 19:43:41.45
スレタイスレ446氏にはこっちのスレで
「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
の数学的側面を語ってもらいたいな。
174:１３２人目の素数さん
12/01/08 20:02:24.92
>>170
勝手な印象だけど、非古典論理と順序数解析とでは、
偏微分方程式と代数幾何くらい論文の多寡が違う気がするな。
175:137
12/01/08 20:04:19.57
>>167
>T|-AならT∪{￢∀ｘA}|-Aで、演繹定理より。
￢∀ｘAが閉論理式でない場合はT∪{￢∀ｘA}が閉論理式の集合で無くなってしまいますが、
それはよいのでしょうか？
176:１３２人目の素数さん
12/01/08 20:19:18.49
どんな公理系を考えているのか知らないけれど、
普通のシステムなら演繹定理に閉論理式という条件は要らないと思う。
177:137
12/01/08 20:34:26.18
そもそもT∪{￢∀ｘA}を公理系と考えることが出来ないのではないでしょうか？
公理系の定義は閉論理式の集合なので。
178:１３２人目の素数さん
12/01/08 21:07:09.40
公理系と考えることが出来なくとも |- は同様に定義できる。
179:１３２人目の素数さん
12/01/08 21:28:19.98
>>170
論文が量産される分野だと、引用される機会も多くなるから、
被引用回数とか G-index, H-index など各種指数も高くなる。
ただ基礎論系の雑誌は、その中でどこかの分野に特化したものは少ないので、
IF は分野の間で格差はそんなにないね。
一番 IF が高い基礎論系の雑誌は Annals of Pure and Applied Logic かね？
180:１３２人目の素数さん
12/01/08 21:47:34.48
>>170 "もはや"ではなくて、当初からそう。
それが数学ではないと言われるゆえん。
181:137
12/01/08 21:50:26.40
>>178
よく分かりました。閉論理式でないといけないと思い込んでいましたが、
意味論と関連付けて考えない限りは
閉論理式に縛られる必要はありませんでしたね。
182:１３２人目の素数さん
12/01/08 21:51:19.38
例えば、岩沢理論。基礎論よりも新しいのに
ずっと深くて重要な進歩がある分野。
これは複数の雑多な分野の総称ではない。
183:１３２人目の素数さん
12/01/08 21:51:50.31
>>67に反論できなくなった奴がまた現れたな。
「一つの分野とは言いがたい」から「数学ではない」って、
さすが追い込まれた奴の発想というか論理展開は独創性溢れてるなｗｗ
184:１３２人目の素数さん
12/01/08 21:54:14.52
>>180 いや、それでも最初期は大きな野望もあって
一つの分野ではあった。しかし、ゲーデル以後、そういった
大きな野望はなくなって、堕落してしまった。
185:１３２人目の素数さん
12/01/08 21:54:37.82
はいはい、また岩澤理論ね、えーとなんだっけ？暗号に応用できるんだっけ？
よくわからないなー。なんにしても>>67に言い返せないのかなあ？
186:１３２人目の素数さん
12/01/08 21:59:12.38
>>183
67って、全然基礎論擁護になっていないじゃん。引用が引用されてて
わけわからん
ちゃんと書きなよ
187:１３２人目の素数さん
12/01/08 22:01:30.82
言い返せってw
あのね、そういうセリフはディフェンディングチャンピオンのセリフよ。
傍流なんだから、打って出ないでいたら、そのまま負けの立場よ
188:１３２人目の素数さん
12/01/08 22:02:15.97
岩沢理論の大きな野望ってなんですか？
この理論だけで一つの分野だとすると、
整数論は「複数の分野の総称」ってことになりますが？
189:１３２人目の素数さん
12/01/08 22:03:30.16
以上、言い返せないバカの負け惜しみでした。
190:１３２人目の素数さん
12/01/08 22:06:57.52
>>188
数学自体が一つの分野であって、本来は切り分けられないけど、
便宜上分けた一部。
身体に対する右腕のような用語。
基礎論屋と話していると、
反論の仕方が負け犬そのもの。
基礎論はこれこれこういう理由で駄目だ、
というと、
いいや、それは違う、こういういいところがある、
という形で反論を期待しているのに、
数学なんて、所詮どの分野もそんなもんでしょ
といった厭世的な答しかかえってこない。
真の数学を知らないんだよな。
191:１３２人目の素数さん
12/01/08 22:10:26.13
このバカは、一つの目標に向かってすべてが進んでいる、
ファシズム的な分野が理想だと思っているらしいな。
ま、若気の至りってやつだろうな。多様性の重要さがわかっちゃいない。
192:１３２人目の素数さん
12/01/08 22:12:27.71
＞真の数学を知らないんだよな。
とか言って逃げないで、その一つの分野である数学の「大きな野望」を解説してくれよ。
いつもごまかして逃げて行くだけじゃないか？
193:１３２人目の素数さん
12/01/08 22:13:47.35
個々の研究者レベルでは、いくつかの方向を向いていて良い。
しかし学問たるもの発展の過程で必ず中心と傍流ができる。これは避けられ無い。
その中心が無数にあったら、それは学問とは呼べない。
194:１３２人目の素数さん
12/01/08 22:15:37.99
基礎論は一つのパラダイムを形成していないんだな。
195:１３２人目の素数さん
12/01/08 22:18:11.70
>>193
ハッタリ乙
196:１３２人目の素数さん
12/01/08 22:21:05.02
>>190
>数学なんて、所詮どの分野もそんなもんでしょ
基礎論屋って皆そんなふうに考えてるの？
だとしたらかなり可哀想な人達
197:１３２人目の素数さん
12/01/08 22:22:43.32
シミュレーションスレのシミュレーションを基礎論に置き換えるとよく分かる
198:１３２人目の素数さん
12/01/08 22:22:45.70
>>196
自演乙
199:１３２人目の素数さん
12/01/08 22:24:38.43
「その中心が無数にあったら、それは学問とは呼べない」とか
「基礎論は一つのパラダイムを形成していないといけない」とか
自分の主観的な仮定に基づく批判をしているようだが、
その仮定は殆どの人間にとって「はあ？」なんだな。
だから別に反論する気も反論する必要も感じない。
200:１３２人目の素数さん
12/01/08 22:29:51.95
基礎論は数理科学で数学じゃない、とか言い張ってたのはどうしたのかなー？
前スレで皮肉られて、言い返せなくなってやめちゃったのー？
201:１３２人目の素数さん
12/01/08 22:31:04.72
>>199
では、>>170
の前半について反論してくれ。
そして基礎論の中心テーマは何？一番大きいものひとつ。
202:１３２人目の素数さん
12/01/08 22:33:00.02
おま、アホか？何が「では」なんだか、サッパリ分からんな。
203:１３２人目の素数さん
12/01/08 22:35:50.18
>>199
ごめん、読み間違えた。読み返してみたら、
やはり、そういったこと全て基礎論では認めちゃっているんだよね。
数学では違うんだよ。
そこにハァ？といってしまうあたりが数学者じゃない。
数学はひとつ。
この理念があるかないかが数学者かそうで無いかを分ける。
204:１３２人目の素数さん
12/01/08 22:37:09.68
数学は一つの有機体なのだが、
そこに基礎論は入っていないということを
認めてしまっているので、
基礎論は数学では無い。
もう合意事項な。
205:１３２人目の素数さん
12/01/08 22:37:17.69
＞真の数学を知らないんだよな。
言ってる本人も知らないだろ、勉強不足で。
いつも抽象的な数学理念ばかり。
206:１３２人目の素数さん
12/01/08 22:39:30.02
たった一度でもいいから具体的な理念を語れば疑念が晴れるのにねえ…
207:１３２人目の素数さん
12/01/08 22:40:42.53
「中心が複数ある一つの有機体」とか「複数のパラダイムが共存する一つの有機体」とか
そういう想像が出来ない時点で視野の狭さを感じるな。
>>191の言うとおり、若気の至りなんだろうから、生暖かく見てるのが一番かね。
208:１３２人目の素数さん
12/01/08 22:42:23.88
いや、こういった合意事項が出来るのは残念なことだが、
それなら俺はもうここでは何も言わない。
言わない理由はシミュレーションスレに書いてあることと基本は同じ。
じゃ、俺は数学して寝る。さいなら。
209:１３２人目の素数さん
12/01/08 22:43:36.05
>>208
具体的に語ってくれれば、すぐにもその合意事項というのを撤回しますよ
210:１３２人目の素数さん
12/01/08 22:45:47.93
逃げちゃったねー。もう来るなよー。
211:１３２人目の素数さん
12/01/08 22:47:04.05
ぐーぐるで「具体的な理念」を探して寝るそうだ。おやすみ。
見つかったらこのスレにコピペしてね。
212:１３２人目の素数さん
12/01/08 22:49:15.89
「基礎論の中でも論文が書きやすい分野と書きにくい分野がある」ということを認めると
「数学はひとつ」という理念を持っていないということになるのなら、
「数学の中で論文が書きやすい分野と書きにくい分野がある」というのもその理念を否定している。
数学の研究現場を知らないアマチュア数学者の臭いがぷんぷんだなｗ
213:１３２人目の素数さん
12/01/08 23:05:02.97
例えば、といいながら出てくるのは岩沢理論だけ。文字通り馬鹿の一つ覚えだな。
工房か？学部生ならもう一つや二つレパートリーがあっても良さそうだし。
214:１３２人目の素数さん
12/01/08 23:10:21.53
>>181
>よく分かりました。閉論理式でないといけないと思い込んでいましたが、
>意味論と関連付けて考えない限りは
>閉論理式に縛られる必要はありませんでしたね。
全称化の規則、気を付けて。
|- の左側に現れる変数を全称化することを禁止しないと、健全でなくなるよ。
215:１３２人目の素数さん
12/01/08 23:25:07.20
>>177
|- は本当は |-_X などの添え字が付く。
このXは推論規則と公理型の集まり。
A |-_X B と書いたとき、
AからXの推論規則と公理型を使ってBを証明できる、を意味する。
このとき、Aは論理式の集合、Bは論理式。
だから別にAの中身が公理でなければならないのではない。
通常の古典論理では、XにHKやLKが入る。
そしてペアノ算術などではXにPAが入る。
だから右側がPAの公理なら、 |-_PA ∀x￢(sx=0) と書いてよい。
しかし |-_PA ￢(0x=0) などは無条件に書けない。
（エルブランの定理が関与する。言語内に定数がない場合がある。）
だから PA |-_PA φ とする必要がある。
ここで左側のPAはPAが定義されている言語上のすべての論理式になる。
もちろんモデルを持たせるには閉論理式である必要がある。
数学書では大抵 PA |- ∀x￢(sx=0) と書かれる。
これは |-_PA を略しているのだが、次のような事例の識別ができなくなる。
PA |-_HK φ ⇔ PA |=_HK φ は成り立つ。
PA |-_PA φ ⇔ PA |=_PA φ は成り立たない。
これは計算機や非古典論理や証明論では致命傷になり得る。
216:１３２人目の素数さん
12/01/08 23:40:17.04
批判されてるうちが華だと思うな。
無視されて消えていくより。
最近見た学部生向け現代数学案内では、いろんな分野を
紹介しているのに、基礎論だけごっそり無かった。
217:１３２人目の素数さん
12/01/08 23:44:27.73
おお、学部生向け案内とかマジでリア工だったのか
218:１３２人目の素数さん
12/01/08 23:48:47.28
>基礎論だけごっそり無かった。
基礎論以外の数学のすべての分野が全部あっただと？そんなわけあるまい。
世の中には無数に分野があるんだ。
そのうち「学部生向け現代数学案内」の類で必ず紹介される分野、
大学によって紹介されたりされなかったりする分野、
まず紹介されない分野とあるわけだが、
日本では基礎論は二つ目に分類される、っていうだけ。
アメリカではまともな大学なら確実に第一分類だろう。
219:１３２人目の素数さん
12/01/09 00:04:37.33
>>218
つまり、日本では無視できるほど格下だと思っていた基礎論が、
アメリカに行って世界を見てみると結構認められていて、
焦った連中がここで憂さ晴らしをしているわけね。
220:１３２人目の素数さん
12/01/09 00:24:04.74
>>218-219
呑気だなー。
221:１３２人目の素数さん
12/01/09 00:31:25.36
>>218
無数にある分野の一個にすぎないの？基礎論って。
222:１３２人目の素数さん
12/01/09 00:34:17.67
もしかして基礎論を擁護する振りして
実はおとしめるという高等技術か？
223:137
12/01/09 01:00:30.34
>>214
はい。
ともかくモデルによる充足関係T|=AとT|-Aの関係を見るときは
Tとして閉論理式の集合のみを考えるようにすれば問題ない、
しかし演繹定理などの構文論の定理は閉論理式という制約のない形で述べておいた方が
使い勝手が良いという理解でよろしいでしょうか？
>>215
Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？
224:１３２人目の素数さん
12/01/09 03:09:20.13
数学のすべての分野は無数にある分野の一つなわけだが。
それが貶めているという風にしか読めないなら小学校から国語をやり直してきな。
>>218、無数にある分野の一個「にすぎない」なんて一言も言っていないわけで、
苦し紛れに相手の発言を捏造するのは見苦しいよ。
225:１３２人目の素数さん
12/01/09 06:18:21.24
>>216
君も相手されている内が華だよ。
馬鹿の一つ覚えやっていると誰も相手しなくなるぜ。
226:215
12/01/09 07:44:56.92
>>223
＞Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？
Xには論理も非論理も両方入ると考えてください。
HKやLKは一般的な一階論理の公理や推論のまとまり。
これにいくつか公理を付け加えたものがPAとなります。
はじめに、言語という使用可能な記号を設定するのですが、
その言語を適当に並べて、「論理式」の条件を満たすような記号列が、
（集合という形で）左側に入ります。
もちろんXに入る公理や推論、右側の論理式でも、言語で設定した記号以外は使用できません。
227:215
12/01/09 07:57:03.84
もう少し直感的に考えると、
ある言語を設定して、その言語を使って作られる論理式がある。
PA |-_PA φ の左側が定義域、右側が値、|-_PA が写像の定義と考えると、
定義域も値もその言語の論理式全体を動くといったイメージ。
228:215
12/01/09 07:59:35.85
訂正：
この説明はよくない。
同じ定義域から複数の値が出現するだろうから。
229:１３２人目の素数さん
12/01/09 12:17:11.15
>>225
え？初めてだよここ書くの。
230:１３２人目の素数さん
12/01/09 15:50:12.96
このスレの
138 ：１３２人目の素数さん：2012/01/06(金) 22:28:15.65
>>128
accessible ordinal (cardinal) の解説希望。
と質問したのだが、未だに回答が無い。
231:１３２人目の素数さん
12/01/09 15:57:22.42
あきらめてググったら？
232:１３２人目の素数さん
12/01/09 17:56:53.11
>>231
もうググったよ。それでも分からん。
ただし、 >>230 を投稿したのは私では無い。
233:１３２人目の素数さん
12/01/09 19:52:48.35
日本人は韓国に来るな
234:１３２人目の素数さん
12/01/09 19:55:21.11
韓国人は日本にくるな
235:１３２人目の素数さん
12/01/09 20:34:25.35
ゆとり民族、ゴミジャップ
236:１３２人目の素数さん
12/01/09 20:57:36.69
関数f(x)がx=aで微分可能なとき、{Af}'(a)=Af'=(a)を証明せよ
できる人いる？
237:１３２人目の素数さん
12/01/10 01:11:47.07
>>230
accessible ordinal (cardinal) = not inaccessible ordinal (cardinal)
なんじゃね？二重否定の除去！
238:１３２人目の素数さん
12/01/10 05:38:37.97
>>232
ぐぐればふつうに出てくるぞ：
URLﾘﾝｸ(en.wikipedia.org)
239:１３２人目の素数さん
12/01/10 10:06:39.78
>>238
いかにも巨大基数と関係が出て来そうな定義だな。
240:１３２人目の素数さん
12/01/10 15:34:56.39
巨大基数と膨大基数の違いをおしえれ
241:１３２人目の素数さん
12/01/10 16:14:01.75
>>235
キムチ野郎
242:１３２人目の素数さん
12/01/11 01:15:54.22
コピペ
75 ：１３２人目の素数さん：2012/01/10(火) 16:38:44.94
ｽﾚﾘﾝｸ(math板:89-94番)
ということなんで選択公理廃止！
以後、決定性公理を採用します。
243:１３２人目の素数さん
12/01/11 02:12:16.17
決定性公理：すべての数学体系は決定可能である。
244:１３２人目の素数さん
12/01/11 02:39:26.08
確かに今の日本はゆとり国家
245:１３２人目の素数さん
12/01/11 04:00:59.17
これが古代史に伝わる数百年に一度、
彼の地に誕生するというスーパーゆとり民族か。
246:１３２人目の素数さん
12/01/11 06:54:52.94
>>54
直観主義数学ではすべての実数値関数が連続ということですが、
ということは実数の集合はすべて可測ということですか？
247:１３２人目の素数さん
12/01/11 16:35:14.91
>>240
字義的には huge cardinal が巨大基数と訳されるべきだろうな。
ま、定着しちまったものは仕方がない。
定訳をおかしいおかしい言っているとマツシンになっちまうしな。
248:１３２人目の素数さん
12/01/11 16:42:57.80
>>247
> 定訳をおかしいおかしい言っているとマツシンになっちまうしな。
で、常識的な公理をおかしいおかしい言ってるとエムシラになるってかｗｗｗ
249:１３２人目の素数さん
12/01/12 01:45:57.67
このスレを見ると、住人に人気があるのは
・様相論理
・証明可能性述語
・巨大基数
みたいだな。選択公理関係もはやってる？
250:１３２人目の素数さん
12/01/12 06:37:25.16
>>246
可測というにはルベーグ測度が定義できないと話にならない。
何かそれっぽいものは直観主義でも定義できるらしいが、
どこまでできればそれをルベーグ測度と呼んでいいのか、という問題になる。
251:１３２人目の素数さん
12/01/12 07:14:54.37
>>238
232はググりもしなかったことが明らかになったな
252:１３２人目の素数さん
12/01/12 07:56:39.56
12 ：１３２人目の素数さん ：2012/01/12(木) 01:18:39.79
数学基礎論・数理論理学 その11
(p)ｽﾚﾘﾝｸ(math板)
の奴らは
(p)URLﾘﾝｸ(www.imub.ub.es)
のような研究集会があった事すら知らん奴が多いようだな
可哀想な数学を知らない人達・・・
253:１３２人目の素数さん
12/01/12 08:01:08.02
すいません、
私は現在統合失調症で職を持たない身なのですが、
明日の論理学の世界に貢献したいと考えております。
そこで以下のように公理系のデータベースの構築をはじめようと考えております。
URLﾘﾝｸ(www4.atwiki.jp)
すべての公理系をクリックすればアウトプットできるような
巨大なデータベースの構築を目指します。
もちろんリンクなどでの立体的なデータ構造を考えております。
データの保管はOracleサーバを考えております。
よろしこお願いします。
254:１３２人目の素数さん
12/01/12 08:06:19.15
また、個々の体系が何を意味しているのかは分かりません。
一アマチュアプログラマーとして皆様に貢献したいです。
上のリストは以前紹介された様相論理のデータベースをもとにしています。
私はマジ基地ですが、よろしこお願いします。
255:１３２人目の素数さん
12/01/12 17:14:23.11
>>252
そいつ（巨大基数スレ12）は232か？
だとすると自分の怠慢を棚にあげてよくもまーｗｗ
256:１３２人目の素数さん
12/01/12 20:06:42.71
>>250
すべての関数が連続ならば、積分を考えるには開集合に測度を持たせられれば十分だろ。
ルベーグ測度なんてのはルベーグ積分の為にあるものなんだから。
直観主義でも開集合には測度を定義できるんですよね？
257:１３２人目の素数さん
12/01/12 21:13:52.74
こんなんあるよ
us.metamath.org/index.html
これの部分構造論理とか線型論理とか様相論理とかのver.があれば
勉強・研究する人には便利だろうな
258:１３２人目の素数さん
12/01/12 21:30:54.87
いちおうE. BishopのConstructive Analysisとか
Foundations of Constructive Analysisとかには
Lebesgue measureが定義してあるみたいだよ
ただ「直観主義数学ではすべての実数値関数が連続」
とかいうときの「実数値関数」とか「連続」という言葉の意味は
普通の数学でいうときのそれとは違うと考えるべきだと思うけどね
A が B より強いというのは A → B が成立して A と B が両立する場合に言うのが
普通なのでそういう意味では片方が他方より強いという関係にはないけど、
数学的公理の部分で、形式的には古典的数学と互いに背反するような
公理ないし定義を採用していることにはなると思う
259:１３２人目の素数さん
12/01/13 00:01:25.37
>>257
なんでそんなめんどくさい貼り方するの？
URLﾘﾝｸ(us.metamath.org)
260:１３２人目の素数さん
12/01/13 01:49:59.23
>>258
>ただ「直観主義数学ではすべての実数値関数が連続」
>とかいうときの「実数値関数」とか「連続」という言葉の意味は
>普通の数学でいうときのそれとは違うと考えるべきだと思うけどね
もっともだとは思うが、
それを言い出すと A → B の意味も直観主義と古典論理では違うし、
何から何まですべて違うことになる。
確かに公理系Tに公理を一つ加えただけで
Tに元々含まれる公理の意味は変わるともいえる、背景が違うのだから。
しかし、ある程度の差異は捨象して同一視してしまって比較するってのが
学問というものじゃないかい？
261:１３２人目の素数さん
12/01/13 02:25:16.86
部分構造論理では最近は何が流行っているのでしょう？
詳しい方、解説をお願いします。
262:１３２人目の素数さん
12/01/13 02:40:34.56
421 ：「名無しわざとか？」とかイヤミを言われた：2012/01/12(木) 08:03:41.44 ID:3+R7T9ps
誰も解答を書かないので>>360の解答を。
連立方程式
{ x-4=y+4
{ x+4=2(y-4)
これを解いてy=20,x=28
Aさんが28個。Bさんが20個。
つーことで、アイジャグの320番台と328番台が高設定だ！
朝から全ツッパしろ！！！
爆死覚悟でやってみてーけど、ヲレ明日は忍者屋敷イカネーといけないので凹
P.S つるかめ算とかやってたような頭の柔らかい小学生とかはもっと簡単に解けちゃうのか？
ｽﾚﾘﾝｸ(slotj板:310-312番)
263:１３２人目の素数さん
12/01/13 06:16:18.84
線型論理も部分構造論理の一つと考えれば、部分構造論理の中で線型論理は断然はやってるね。
264:GMG ◆.5wljPk1.c
12/01/13 08:29:02.49
180=nα+B=B+(n-1)α＋α
265:１３２人目の素数さん
12/01/13 18:24:27.23
Lukasiewicz 論理をよく聞くかな。部分構造論理の中では直観主義論理に次いで綺麗な構造らしい。
URLﾘﾝｸ(en.wikipedia.org)
266:１３２人目の素数さん
12/01/13 18:29:14.69
古典命題論理をストローク一本、公理一本で展開することに何かメリットある？
267:１３２人目の素数さん
12/01/13 18:40:40.82
そら時と場合によるだろう。かなり特殊だけど役に立つ場面はあるだろうね。
268:１３２人目の素数さん
12/01/13 20:34:54.20
次の性質を持つ集合 x は一般に何と呼ばれているのですか?
∀y∀z [ [x ∋ y ∋ z ] ⇒ [ x ∋ z ] ]
269:あのこうちやんは始皇帝だった
12/01/13 20:38:02.94
>>268
ニートの、ゴミ・クズ・カスの、クソガキ！！！！！！！！！
270:スレタイ446
12/01/13 21:24:28.35
遺伝的集合とか推移的集合じゃないの？
271:１３２人目の素数さん
12/01/13 22:15:53.14
メンバーのメンバーはメンバーなり。
272:１３２人目の素数さん
12/01/13 22:16:38.49
昔懐かし稲垣メンバー。
273:１３２人目の素数さん
12/01/13 22:28:49.43
>>270
ググってもそれらしき物は出て来なかったが。
274:１３２人目の素数さん
12/01/13 23:31:01.63
>>273
英語てググりなさい
275:１３２人目の素数さん
12/01/13 23:59:55.45
hereditary set, transitive set でググったら、
URLﾘﾝｸ(en.wikipedia.org)
が有った。
しかしその意味合い (定義では無くて背景などの関連事項) が良く分からない。
276:１３２人目の素数さん
12/01/14 04:18:22.31
>>127
巨大基数の表なんざ、ぐぐればすぐに出てくるぞ：
URLﾘﾝｸ(en.wikipedia.org)
277:１３２人目の素数さん
12/01/14 04:40:42.26
>>276
29 種類どころか僅かしか無かった。
278:１３２人目の素数さん
12/01/14 05:12:44.76
どう見ても29種類以上、書いてあるけどな
279:１３２人目の素数さん
12/01/14 06:05:32.06
>>275
関係Rが推移的とは
∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]
280:１３２人目の素数さん
12/01/14 06:57:56.92
お、スレタイスレ446氏が降臨している！リクエストをコピペしとく。
173 ：１３２人目の素数さん：2012/01/08(日) 19:43:41.45
スレタイスレ446氏にはこっちのスレで
「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
の数学的側面を語ってもらいたいな。
281:１３２人目の素数さん
12/01/14 07:20:03.82
>>279
＞関係Rが推移的とは ∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]
∀x∀y∀z [ [ [x R y ] & [ y R z ] ] ⇒ [ x R z ] ]
ぢゃないのか？
282:１３２人目の素数さん
12/01/14 07:26:00.16
∀xがあるかないかの違いしか見つけられんが
283:１３２人目の素数さん
12/01/14 07:55:28.45
1. inaccessible
2. alpha-inaccessible
3. hyper-inaccessible
4. Mahlo
5. alpha-Mahlo
6. hyper-Mahlo
7. reflecting
8. weakly compact
9. Pi^n_m-indescribable
10. totally indescribable
11. lambda-unfoldable
12. unfoldable
13. v-indescribable
14. lambda-shrewd
15. shrewd
16. ethereal
17. subtle
18. almost ineffable
19. ineffable
20. n-ineffable
21. totally ineffable
22. remarkable
23. omega-Erdos
24. 0-sharp
25. omega_1-Erdos
26. almost Ramsey
27. Jonsson
28. Rowbottom
29. Ramsey
30. ineffably Ramsey
31. measurable
284:１３２人目の素数さん
12/01/14 08:01:54.67
32. 0-dagger
33. lambda-strong
34. strong
35. tall
36. Woodin
37. weakly hyper-Woodin
38. Shelah
39. hyper-Woodin
40. superstrong
41. subcompact
42. strongly compact
43. supercompact
44. eta-extendible
45. extendible
46. Vopenka
47. almost huge
48. super almost huge
49. huge
50. superhuge
51. n-superstrong
52. n-almost huge
53. n-super almost huge
54. n-huge
55. n-superhuge
56. I3
57. I2
58. I1
59. I0
60. Reinhardt
285:１３２人目の素数さん
12/01/14 08:09:56.67
>>283-284
乙。大体のは聞いたことあったけど、数えてみると60もあるんだ。
他に俺の知ってるのは hypermeasurable とかかな。
286:１３２人目の素数さん
12/01/14 08:25:15.60
weakly inaccessible とか strongly inaccessible とかは？
287:１３２人目の素数さん
12/01/14 08:34:30.11
どうしてこうもググりもしない教えてクンが多いのか
288:１３２人目の素数さん
12/01/14 10:33:29.38
>>284
dagger が無いんだが・・・と書こうとしたら次に出て来た。
289:１３２人目の素数さん
12/01/14 16:42:22.90
>>252
巨大基数厨の諸君に告ぐ。
巨大基数の集合論とその応用 そのアレフ 0
ｽﾚﾘﾝｸ(math板)
290:１３２人目の素数さん
12/01/14 20:12:09.02
>>275
公理的集合論では与えられた集合が推移的じゃないと
困る場面が山のようにある
順序数は普通、∈で整列順序付けされる推移的集合として定義される
与えられた集合と同型な推移的集合を作るテクニックとかもある
291:１３２人目の素数さん
12/01/14 20:13:31.75
巨大基数スレも乱立かよ。
マツシンといい、やっぱり基礎論はトンデモ多発分野なだけある。
292:１３２人目の素数さん
12/01/14 21:47:13.19
>>291
マツシンて誰？
293:１３２人目の素数さん
12/01/14 21:51:36.40
>>292
>>141あたりを参照
294:１３２人目の素数さん
12/01/14 23:08:59.21
>>101
巨大基数公理も、幾らでも新たな公理を作ろうと思えば作れる。
研究と称して、そういった公理のお決まりの性質（○○基数から導けて△△基数を導く等々）を
これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。
よってそれらをすべて網羅する必要があるとは思われない。
295:１３２人目の素数さん
12/01/14 23:09:39.74
>>293
2003年ってもう9年前じゃん。バカじゃね？
296:１３２人目の素数さん
12/01/14 23:13:08.90
8年ぶりにマツシンが活動期に入ったんだろ
297:１３２人目の素数さん
12/01/14 23:21:45.54
>>290
テクニックって一階？二階？三階？
298:１３２人目の素数さん
12/01/14 23:44:02.56
>>294
ネタにマジレスですまんが、
そういう研究で論文が通ったのは精々80年代まで。
いまどきそれだけじゃ、査読を通らん。
非古典論理に比べてかなり健全だろ？
299:スレタイ446
12/01/15 00:05:24.66
>>280
レシュネフスキーの数学理論は現在の記述論理にかなり近い。
プロトセティックは型理論のようなもので、
オントロジーは真偽ではなく存在の有無を実現するためのε記号を扱う論理学。
aεb（aはbである。）。
この上にメレオロジーを定義してクラスClを実現する。
（「クラス－真のクラス」は集合とならない、実際にはGBの断片＋α）
グッドマンの方はこのメレオロジーの変種の個体計算などを形式化してる。
300:１３２人目の素数さん
12/01/15 01:13:40.04
いくつかシツモソ
＞この上にメレオロジーを定義してクラスClを実現する
クラスCIってなんですか？
＞実際にはGBの断片＋α
どういう断片ですか？αは具体的には？
301:１３２人目の素数さん
12/01/15 02:22:08.13
>>296
マツシンは8年間活動自粛してたわけではないぞ。
その間も他人のブログのコメント欄なんかを中心に精力的に活動してた。
302:１３２人目の素数さん
12/01/15 03:13:55.87
>>298
巨大基数の健全性ｗ
303:１３２人目の素数さん
12/01/15 04:02:33.74
マツシンタンとかエムシラとかsikiとか人生とか長生きしてるよな。今井は生きてる？鑑定団に出たあたりまでは確認したけど。
304:１３２人目の素数さん
12/01/15 05:52:42.90
このスレが巨大基数について一番専門的な話をしているようなので、質問です。
large large cardinal (大巨大基数?)とか
small large cardinal (小巨大基数?)とか
middle large cardinal (中巨大基数?)とか
ってそれぞれどの基数ですか？
305:１３２人目の素数さん
12/01/15 06:22:31.35
large small cardinal とか small small cardinal とかってなんですかｗｗ
306:１３２人目の素数さん
12/01/15 07:37:38.92
>>294
前半部分は全くその通りだが
「...というオリジナリティのかけらもない論文が多すぎる」というのは
現状をまるっきり分かっていない奴の言うこと。
そんな論文見かけたことすらないね。
307:１３２人目の素数さん
12/01/15 08:15:59.80
ネタにマジレスかこわるい
308:１３２人目の素数さん
12/01/15 08:48:03.56
>>304
URLﾘﾝｸ(ncatlab.org)
ここ見ると31の measurable cardinal が境界だそうだ。
だから 1-30 が small large cardinal で
32-60 が large large cardinal なんじゃないの？
middle large cardinal って聞いたことないけど、measurable のこと？
309:１３２人目の素数さん
12/01/15 13:57:59.29
>>296 >>301 >>303
何年間も同じ奴を追っかけて・・・ヒマだなおまえら。
310:１３２人目の素数さん
12/01/15 14:04:05.75
logic systemのリスト化...ソフトウェアにするか動的ウェブで実現するか...
311:１３２人目の素数さん
12/01/15 16:17:21.91
追っかけなくても勝手に現れに来るからｗ
312:１３２人目の素数さん
12/01/15 20:05:32.35
>>308
Stanford Encyclopedia of Philophy の Koellner の記事
(URLﾘﾝｸ(plato.stanford.edu))から引用：
A large cardinal is small if the associated large cardinal axiom can hold in Gödel's constructible universe L,
that is, if “V ⊨ κ is a φ-cardinal” is consistent, then “L ⊨ κ is a φ-cardinal” is consistent.
Otherwise the large cardinal is large.
この定義によると24のゼロシャープはもう large large cardinal のはずだが。
313:スレタイ446
12/01/15 20:29:39.02
>>300
クラスClは
(a,b)(a＝b≡C(a)＝C(b))
cl(a)≡(Ex)(a＝C(x))
で、定義される。このEは1階論理の量化記号みたいなもの。
Clは何らかの個体の集まりなんだけど、
その集まりの集まりは元の集まりと変わらない。というのが彼のクラスの特徴。
こうすると最上位概念の存在によって循環がなくなる。
1項述語Cl,Ob,二項述語∈,＝が存在して、
・等号＝に関する公理
・外延性公理 (a,b)(cl(a)(cl(b))→(x)(x∈a≡x∈b)→a＝b)
・(a,b)(a∈b→ob(a)(cl(b))
・内包性公理 (Ea)(cl(a)((x)(x∈a N≡ob(Y).ψ(x))))
GodelとBernaysの公理的集合論の断片になる。
あとはクラスclとobに関する操作が多少加わる。
とはいえ、集合論いらない数学は
Feferman・Aczelの構成的数学などもある。
それらをオントロジーの枠組みで実現しているものだろう。
314:１３２人目の素数さん
12/01/15 20:58:47.50
>>312
0^\sharp は cardinal ではないからその定義は意味をなさない罠ｗｗ
315:１３２人目の素数さん
12/01/16 01:16:26.67
>>304
俺は>>308の流儀と>>312の流儀、どちらも聞いたことがあるけど、
きんちんとした定義はないんじゃないかな？
だから23までが small large cardinal
32以降が large large cardinal でいいんじゃない？
ついでにその間の24-31が middle large cardinal とか新説を唱えてみる。
316:１３２人目の素数さん
12/01/16 06:53:15.92
>>313
その理論の強さはどれくらい？ZFC より弱いの強いの？
317:１３２人目の素数さん
12/01/16 08:14:12.21
>とはいえ、集合論いらない数学は
>Feferman・Aczelの構成的数学などもある。
>それらをオントロジーの枠組みで実現しているものだろう。
「それら」は何を指していますか？「実現している」の主語はなんですか？
スレタイスレ446氏のレスは相変わらず読みにくいんですが。
318:１３２人目の素数さん
12/01/16 08:38:47.03
コアモデルがあるような巨大基数は小さいとか言ってみるテスト
319:１３２人目の素数さん
12/01/16 09:34:52.00
?してみるテストって久しぶりに見たw
320:１３２人目の素数さん
12/01/17 02:32:53.13
>>314
κ is a 0-sharp cardinal if there is a non-trivial elementary embedding j: L → L whose critical point is κ
と定義すれば>>312の定義が適用できる！
321:１３２人目の素数さん
12/01/17 06:40:24.56
つまり、0-sharp cardinal は cardinal でないこともあるってことだね。
322:１３２人目の素数さん
12/01/17 17:16:10.88
312の定義に意味を持たせるには
if“V ⊨ κ is a φ-cardinal”then“κ is in L”
であればいいので、“κ is cardinal”である必要はないのね。
323:１３２人目の素数さん
12/01/18 01:46:48.73
>>321, >>322
普通に>>320は、最初に「For a cardinalκ, 」を補えばいいだろうが！
324:１３２人目の素数さん
12/01/18 04:32:03.92
基礎論最大の未解決問題ってなんなのでしょうか？
325:１３２人目の素数さん
12/01/18 05:51:34.40
>>323
では 0-sharp cardinal の存在と（通常の意味の）0-sharp の存在は同値？
326:１３２人目の素数さん
12/01/18 08:50:07.59
>>324
間違いなく「P対NP問題」でしょう。
基礎論の各分野での最大の未解決問題となると、分かりませんが。
327:１３２人目の素数さん
12/01/18 17:46:55.71
>>325
Silver indiscernible は順序さえ保てば自由に動かせて
非可算基数はすべて Silver indiscernible なのだから、
critical point を特定の非可算基数になるような
L から L への elementary embedding なんて
(0^\sharp の存在から)簡単に作れる。
328:１３２人目の素数さん
12/01/18 18:30:36.14
自動定理証明系で
証明仮定（証明図）がすべて出力できるソフトウェアはありますか？
329:１３２人目の素数さん
12/01/18 19:17:07.58
>>328
自分で作れば良い。全ての図を少しずつ列挙し、
同時に一方ではそれらが証明図になって居るかどうか少しずつ判定すれば良い。
330:１３２人目の素数さん
12/01/18 19:39:04.24
>>329
それって普通の対話型証明ソフトと変わらないですよね？
私は公理からの論理式のシーケント列を見たいのです。
331:１３２人目の素数さん
12/01/18 23:53:47.48
３２８の件 スルー お願いします
332:１３２人目の素数さん
12/01/19 01:45:57.11
>>327の言う通りなので、
κ is a real-sharp cardinal if for any a⊂ω, there is a non-trivial elementary embedding j: L[a] → L[a] whose critical point is κ
と定義すれば、“∀a⊂ω(a-sharp exists)”も real-sharp cardinal の存在と同値になって>>312の定義が適用できる！
dagger についても同様。
333:１３２人目の素数さん
12/01/19 03:32:01.91
>>326
> >>324
> 間違いなく「P対NP問題」でしょう。
P≠NP?問題は計算機科学の問題で基礎論の問題じゃないだろが。
そいつを基礎論の問題なんて言ったら「問題を横取りするな」って計算機屋が怒るぞ。
そもそも数学の基礎付けとは全く無関係な問題だ。
そのうち、代数屋あたりが解きそうだな。
結局、ロジシャン自慢のBounded Arithmeticでは歯が立たなかったし。
334:１３２人目の素数さん
12/01/19 04:12:12.63
また「基礎論＝数学の基礎付け」とか言う香具師がでてきなすった。
隔離スレが過疎っちまって構って欲しいのか？
335:１３２人目の素数さん
12/01/19 06:15:01.51
>>312の定義を適用するために、
通常では何らかの性質を持つ基数の存在として記述されない巨大基数公理を
そういう形に書き換えてたいようだけど、
そもそも>>312の定義がおかしくないかい？
“is consistent”というメタレベルの言明を挟んでいるのだから、
“V ⊨ κ is a φ-cardinal”と“L ⊨ κ is a φ-cardinal”で出てくる
二つのκが同じもの、というのが意味をなさないよ。正しくは
if “V ⊨ ∃κ(κ is a φ-cardinal)”then“L ⊨ ∃κ(κ is a φ-cardinal)”
ではないかな？
336:１３２人目の素数さん
12/01/19 06:18:15.00
間違えた、正しくは
if “V ⊨ ∃κ(κ is a φ-cardinal)” is consistent, then so is “L ⊨ ∃κ(κ is a φ-cardinal)”
ではないかと。
337:１３２人目の素数さん
12/01/19 08:04:14.89
大学入ったら基礎論やりたいんですがまず何を勉強したらいいですか？
細かい分野としては逆数学とか証明論などに興味があります、よろしくお願いします
338:１３２人目の素数さん
12/01/19 08:37:31.42
>>337
まず君がいまどのレベルなのか教えてくれないと、アドバイスしようがないだろ。
339:１３２人目の素数さん
12/01/19 08:59:26.46
>>333
Bounded Arithmetic で歯が立っていないのは事実だが、
かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。
そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、
常に他分野の技術によって解決される可能性は開けている。
よって、未解決問題がどの分野に属しているかは、
その問題自体がどの分野の言葉で記述されているかで決めるべき。
ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある
理論計算機科学の問題。
340:１３２人目の素数さん
12/01/19 09:42:40.42
巨大基数スレが二つも乱立しているというのに、
巨大基数ネタで一番盛り上がっているのは結局このスレというのは、
なぜなのだろう？
341:１３２人目の素数さん
12/01/19 13:34:20.78
結局みんなアスペが嫌いなのよ。
巨大基数スレは、アスペが独立スレ立てろと言い出したから、
なんとなくみんなそっちに書きたがらないｗ
342:１３２人目の素数さん
12/01/19 16:51:42.44
>>339
チンコに歯立てるなよ
343:１３２人目の素数さん
12/01/19 19:44:37.71
一般向けの本で、高校レベルの知識で理解可能と書いてあるのに、
実際読んだら？の嵐だったよ。
いきなり「標準形」って出てきてどんどん展開していく。
そこに「標準形」の説明はない。俺には理解できなかった。
やさしい入門書あったら、教えてね。
344:１３２人目の素数さん
12/01/19 21:30:53.85
入門書で金をどぶにすてることから「がくもん」がはじまるのかな
自分で失敗したほうが身につくと思われます んちって
345:１３２人目の素数さん
12/01/20 04:23:36.09
>>343
齋藤正彦 数学の基礎―集合・数・位相 (基礎数学)
で肩慣らししてみたら？（基礎論やらなくても必要な部分）
346:１３２人目の素数さん
12/01/20 04:41:38.68
>>341
アスペだけじゃなく、スレ立てた主も、
教えてもらおうって相手を見下してる偉そうな香具師だったからな。
あっちのスレでアホ丸出しのタワゴトをのたまっているが、
誰も好き好んであのスレ主の相手したいとは思わんだろ。
347:１３２人目の素数さん
12/01/20 07:32:42.59
>>333>>339
ゲーデルがテューリングがでてきたころ、そのような問題がふれている
ということが書いてあるのを読んだことがある。だから、古い問題では
あるのだけれど、計算機科学ができてから特に大きな問題になったと
いうことだろう。
348:１３２人目の素数さん
12/01/20 12:43:08.27
>>339
> >>333
> Bounded Arithmetic で歯が立っていないのは事実だが、
> かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。
> そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、
> 常に他分野の技術によって解決される可能性は開けている。
>
> よって、未解決問題がどの分野に属しているかは、
> その問題自体がどの分野の言葉で記述されているかで決めるべき。
P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。
計算機科学が数理論理学と関係なく生み出して来た言葉で書けるぞ。
Boolean Circuitなんて考え方は基礎論とは全く独立な発想だからな。Razvorovも代数屋だし。
> ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある
> 理論計算機科学の問題。
理論計算機科学が数理論理学の一分野という認識はお前みたいな基礎論屋の勘違い。
夜郎自大の基礎論屋らしい勘違いというか誇大妄想ではある。
理論計算機科学にはむしろ代数の辺境分野とでも呼ぶべき言語理論なども重要なコアパートとして含まれるし
普遍代数や圏論の応用分野でもあるのだから、理論計算機科学は数理論理学の一分野なんかじゃない。
むしろロクな問題もなくロクにポストもなかった基礎論屋が「計算機がらみなら問題も色々あるしメシも食えそう」って
理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。
基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とかが
計算機言語の型システムの高度化にも使えるという計算機屋の仕事が計算機科学側で流行り出してから、
慌てて基礎論屋が飛び付いてつまみ食いして計算機科学的には何の使い物にもならない瑣末な視点の論文を基礎論屋が粗製乱造して来たのが実態じゃないか。
型理論の論文は基礎論屋が乱入して来てからロクなのが出ていない。ずっと昔からやっていたMartin-L\"ofとかには当然ながら俺も敬意を表するが。
349:１３２人目の素数さん
12/01/20 15:04:28.57
>P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。
>計算機科学が数理論理学と関係なく生み出して来た言葉で書ける
頑張れば書けるよね、それがどうした？
代数の問題だって頑張って幾何の言葉や解析の言葉で書きなおせる場合が多い。
だからその問題が幾何や解析の問題だと言い出せばのはこじつけ。
>理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。
>基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とか
君の「俺様歴史観」によるとそういうことになるわけね。
あほらしくてわざわざ反論する気もしないな。
350:１３２人目の素数さん
12/01/20 15:50:37.80
>>335-336
κを定数記号だと理解すれば、>>312はそのままで>>336の意味になると思うがの
351:１３２人目の素数さん
12/01/20 18:43:54.93
>>346
>あっちのスレでアホ丸出しのタワゴトをのたまっている
いや全く。
巨大基数（的）性質なのに、名前付けるのに「存在すれば」という仮定つけてる、
なんてのは巨大基数のなんたるかがまるっきり分かっていない証拠。
巨大基数に手を出す前にもっと勉強すべきことがあるだろう、って話。
352:１３２人目の素数さん
12/01/20 19:00:06.15
>>345
ポチらせていただきました。どうもです。
353:１３２人目の素数さん
12/01/20 19:20:12.86
>>350, >>336
俺は>>312の記述が間違っていて、
ZF(C) |- (∀κ:cardinal)[κ is a φ-cardinal → L ⊨ (κ is a φ-cardinal)]
が small large cardinal の定義だと思っていた。
これだと０♯とか、そのままでは適用できなくなるでしょ？
354:１３２人目の素数さん
12/01/21 05:23:41.09
結局、small large cardinal とか large large cardinal とかってなんなの？どの定義が正しいワケ？
355:１３２人目の素数さん
12/01/21 07:05:59.08
スレタイスレ446氏はその後出てこないの？
また新たなネタをもたらしてくれることを期待しているんだが。
356:１３２人目の素数さん
12/01/21 08:16:43.86
自演乙
357:１３２人目の素数さん
12/01/22 14:15:58.07
BBQ が止まっています
BBX が止まっています
ほんとに？
358:１３２人目の素数さん
12/01/22 23:14:40.29
>>353
実際にいままでに提案された巨大基数公理については、どっちの定義でも同じこと。
確かにゼロシャープとかの場合は、ちょっと定義をいじらないといけないけどね。
359:１３２人目の素数さん
12/01/25 01:20:09.09
スレタイスレ446氏まだー？
360:１３２人目の素数さん
12/01/25 06:40:43.46
数学基礎論は、哲学的問題に数学を持ち込んだという意味で「数理哲学」と呼ぶべきものだと思う。
「数学に関する哲学」という意味での「数理哲学」は、一般的な「数理○○学」の用法から逸脱していて適切ではない。
361:１３２人目の素数さん
12/01/25 12:10:51.99
生命とか国家について考えてるわけじゃないから哲学とまではいかないだろう。
論理学のうち数理的にやれる部分を数理論理学と呼び、研究の発展とともに「数理的」の内容が変わっていく、って感じじゃないの？
362:１３２人目の素数さん
12/01/25 13:53:11.26
はっきり言って哲学とは関係ない。
皆、やりたいことをやっているだけ。
363:１３２人目の素数さん
12/01/25 13:55:59.49
世界 50 億人誰にでも分かる表現が可能なのが数学。
そうで無いのが哲学。
364:１３２人目の素数さん
12/01/25 14:27:17.77
>>363
それはハッタリ的アフォリズムでしかない
365:１３２人目の素数さん
12/01/25 15:00:35.87
阿保リズム
366:１３２人目の素数さん
12/01/25 15:08:25.72
>>361,363
現代哲学には大陸哲学と分析哲学があります。
生命や国家について語り人類に共通な真理とは限らないのは大陸哲学です。
擬似問題を切り捨て明晰さを重視し自然科学と親和性が高いのが分析哲学です。
数学の哲学は分析哲学の一分野です。
大陸哲学
URLﾘﾝｸ(ja.wikipedia.org)
分析哲学
URLﾘﾝｸ(ja.wikipedia.org)
数学の哲学
URLﾘﾝｸ(ja.wikipedia.org)
367:１３２人目の素数さん
12/01/25 15:23:12.95
>>366
ならなんでやたらドイツ語の基礎文献が多いんだ？
368:367
12/01/25 15:37:44.69
ごめん、ちゃんと読んでなかった。
撤回する。
369:１３２人目の素数さん
12/01/25 19:50:41.64
哲学なら現代と限定するのはそもそもおかしくね
370:１３２人目の素数さん
12/01/25 21:10:33.17
そのへんは、数学を現代数学と限定するのが本来おかしいのと一緒でしょ
最近有名になったサンデルとかの政治哲学とかも分析哲学よりだし
国家や生命についての問題は疑似問題に過ぎないというと語弊があるけどね
371:１３２人目の素数さん
12/01/26 01:16:15.74
>>361
そうやって数学の扱える範囲を拡げたのが基礎論の大きな功績の一つ。
>>363
仮に「哲学」と「数学」の違いをそう定義するのなら、
基礎論以前には「哲学」でしか扱えなかったものが
基礎論によって「数学」として扱えるようになった、ということ。
372:１３２人目の素数さん
12/01/26 07:54:25.48
-P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment).
P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB).
から
P(e(x,x)) # label(Reflexivity).
を証明。
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 3.04 (+ 0.20) seconds: Reflexivity.
% Length of proof is 19.
% Level of proof is 8.
% Maximum clause weight is 48.
% Given clauses 588.
1 P(e(x,x)) # label(Reflexivity) # label(non_clause) # label(goal). [goal].
2 -P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment). [assumption].
3 P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB). [assumption].
4 -P(e(c1,c1)) # label(Reflexivity) # answer(Reflexivity). [deny(1)].
5A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
5 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w)). [resolve(5A,a,3,a)].
6A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
6 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5)),v6)). [resolve(6A,a,5,a)].
7A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u))) | P(w). [resolve(2,a,5,a)].
7 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w))). [resolve(7A,a,3,a)].
9A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5))) | P(v6). [resolve(2,a,6,a)].
9 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6),e(v5,v6))). [resolve(9A,a,3,a)].
10A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)].
10 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x))). [resolve(10A,a,7,a)].
373:１３２人目の素数さん
12/01/26 07:55:12.82
11A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
11 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5)),v6)). [resolve(11A,a,7,a)].
14A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)].
14 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5))). [resolve(14A,a,3,a)].
28A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x)). [resolve(2,a,10,a)].
28 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),e(e(e(e(v5,e(e(e(v5,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)))). [resolve(28A,a,7,a)].
35A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5))) | P(v6). [resolve(2,a,11,a)].
35 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),v6),e(v5,v6))). [resolve(35A,a,3,a)].
57A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
57 P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6)),v7)). [resolve(57A,a,14,a)].
374:１３２人目の素数さん
12/01/26 07:56:01.55
141A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)). [resolve(2,a,14,a)].
141 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),v6),v7),e(v6,v7)),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). [resolve(141A,a,35,a)].
262A -P(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6))) | P(v7). [resolve(2,a,57,a)].
262 P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10)),e(v9,v10))). [resolve(262A,a,28,a)].
589A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6)) | P(e(v5,v6)). [resolve(2,a,9,a)].
589 P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),v5),e(w,v5)),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). [resolve(589A,a,141,a)].
1754A -P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10))) | P(e(v9,v10)). [resolve(2,a,262,a)].
1754 P(e(x,x)). [resolve(1754A,a,589,a)].
1755 $F # answer(Reflexivity). [resolve(1754,a,4,a)].
============================== end of proof ==========================
1階論理の証明は省略してもここまでの分量になる。
375:１３２人目の素数さん
12/01/26 20:46:23.39
できたら正誤表もヨロ
・・・ともかくGJ・・・感謝
376:１３２人目の素数さん
12/01/27 05:17:56.94
巨大基数の数理哲学的な説明ってどうなってるの？
377:１３２人目の素数さん
12/01/27 17:09:37.81
__ﾉ)-'´￣￣`ｰ- ､_
, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
378:１３２人目の素数さん
12/01/27 17:11:12.67
誰もお前みたいなブスとは付き合いたくねえ。
379:１３２人目の素数さん
12/01/27 18:49:12.14
>>375
何に感謝したの？？
380:１３２人目の素数さん
12/01/27 20:32:41.33
ざっくり言って、第二不完全性定理は、もちろん第一不完全性定理の系で、
第一不完全性定理は不動点定理の単なる系なのだが、その不動点定理も、さらに
なにかメタな洞察があって、そこからみれば自明な定理である、なんていう話は
聞いたことあるかな？
381:１３２人目の素数さん
12/01/27 20:50:55.45
証明の仕方によっては
系になり得るけど
第二は第一と無関係に証明できるし
第一も不動点定理と無関係に証明できるからなぁー
382:１３２人目の素数さん
12/01/27 22:09:35.94
>>381
たしかにそりゃそうなので前段は余計なことを言ったかもしれん。
ただ、オリジナル（ゲーデル）では380で書いた順番だったから
それが一番自然な順序と言えなくもないだろう？
まあそれはよいとして、後段の、不動点定理が成り立つのはそりゃ当然だ、
と見えるようなメタな定理ってあるんかな？しつこくてすまんが。
383:１３２人目の素数さん
12/01/27 23:06:23.03
対角線論法や自己参照のイメージで良い。
似たような論法は計算論全般でよく出てくる。
384:１３２人目の素数さん
12/01/27 23:48:39.49
>>383
それは分かるのだが、たとえば、ブラウワの不動点定理とラムダ計算における不動点定理に
共通する成立条件は何なのだろうか？あるいはこうした不動点定理を最も抽象化した定理って
どんな形をしているんだろうか？という疑問なのだが。おかしいか？
385:１３２人目の素数さん
12/01/27 23:59:52.04
λ計算は数学の関数の性質をすべて抜き出せるからなぁ。
共通する性質はある程度の算術が作れるってところか。
386:１３２人目の素数さん
12/01/28 00:12:55.57
>>384 >>385
圏論ではそういう抽象化をやってないか？
387:１３２人目の素数さん
12/01/28 00:18:05.71
やってます。
過去スレでも話題になってます。
388:１３２人目の素数さん
12/01/28 00:28:57.03
>>387
スマン。どのあたり？
389:１３２人目の素数さん
12/01/28 09:43:01.73
圏論好き集まれスレで話題になってるよ。
390:１３２人目の素数さん
12/01/28 10:13:27.53
>379
萌え材につかいましたが・・・やはり問題あり?
391:１３２人目の素数さん
12/01/28 11:13:10.57
>>386
>>387
>>389
Lawvereの定理のことを言ってるんだとしたら、あれはゲーデルや通常の不動点定理を
それほど抽象化したものにはみえない。記法を換えただけにみえるのだが。
392:１３２人目の素数さん
12/01/28 15:47:01.46
おほほ猫
393:猫釣りは餌が重要 ◆MuKUnGPXAY
12/01/28 17:39:40.18
ケケケ猫
394:389
12/01/28 18:44:03.24
>>391
同感。
結局は対角線論法が根源的な説明に思える。
395:１３２人目の素数さん
12/01/28 18:45:33.95
>>393
あんた全てのスレッドを監視しとんのか？
あんたとは無縁じゃろう、この話題は。
396:猫釣りは餌が重要 ◆MuKUnGPXAY
12/01/28 18:58:07.71
>>395
何処を監視するのかは私の勝手なのでね。
猫
397:１３２人目の素数さん
12/01/28 22:28:45.86
こんばんは。初めて書き込むのですが、論理学の質問をしたいと思って
ネット上を探していたらここにたどりつきました。ご助力願います。
質問 Ｌｐの論理式でないのはどれか。
(1)∀w∀x∃zＲ(x,z)
(2)∀xＰx⊃∀xＲ(x,c)
(3)∀xＰx⊃∀cＲ(x,c)
(4)∀z∀x(∀xＰx⊃∀zＲ(zz))
です。出題の意図がわかりかねまして質問しました。
どうぞよろしくお願いします。
398:１３２人目の素数さん
12/01/28 22:41:40.23
「Ｌｐの論理式」という表現は、貴方の持っている本特有の言葉遣いだと思われます。意味がわかりません。
399:１３２人目の素数さん
12/01/28 22:47:25.20
すみません。
どうやらLpというのは「初等論理の言語」を表しているようで、
⊃、￢、∧、∨、∀、∃を表すようです。
400:１３２人目の素数さん
12/01/28 23:00:42.69
>>397
本？それとも講義？
本なら書名を教えてくれない？
401:１３２人目の素数さん
12/01/28 23:12:03.45
講義です。
その先生が独特に使うのでしょうか…。
もう途中から何言ってるのか、って感じで困ってたんです。
最後に課題を出されまして…。
専門ではなく教養なので、おそらくそこまで難しいことは言ってないとは
思うですが…。
402:１３２人目の素数さん
12/01/28 23:21:09.89
>>397
素直に考えると
4番が量化記号がダブって束縛しているのでおかしいけど、
論理式の定義によるからなぁ
403:１３２人目の素数さん
12/01/28 23:32:22.22
397です。レスありがとうございます。
もうすこし追記します。その先生によると
Lpの論理式（Ｆ）とは、次の(1)～(4)を繰り返し適用して構成される
有限の記号列のことである。
(1)各atomic formula αはＦである。
(2)αはすでにＦであるとわかっている⇒（￢α）もＦである。
(3)α,β∈Ｆ⇒(α⊃β）,(α∧β）,（α∨β）∈Ｆ
(4)α∈Ｆ⇒（∀xα）∈Ｆ
というのが定義のようです。
素人にゆっくり教えてやろうという講義ではなく、先生の独り言的な講義
だったため、素人のこちらは全くわかりませんでした…。
404:１３２人目の素数さん
12/01/28 23:39:56.36
>>403
わきからごめん。
>もう途中から何言ってるのか
こういう状態でこの宿題だけやっても、という気はするが、参考までにコメントするよ。
｢Ｌｐの論理式である｣というのは、直感的には，｢文法に合った式である｣という意味だよね。
ここに貴方が書いた定義に照らすとすれば、(1)-(4)はどれも文法に合っていると思う。
しかし、ふつうの定義では，(1)(2)は（かろうじて）文法に合っているが、(3)(4)は文法に
合っていない（Lpの論理式でない）と思われる。というのは、，(3)は定数cが限量変数に
使われているし、(4)は（402も言うように）zとxが限量変数としてダブって使われている
から。どうかな？
405:１３２人目の素数さん
12/01/28 23:44:17.61
>>403
その定義だと1が論理式じゃないね。
∃記号が￢∀￢と交換できないなら。
406:１３２人目の素数さん
12/01/28 23:53:13.97
皆さん、ありがとうございます。
404さんもおっしゃる通り、この状態では…ということはわかっていますが、
どうしてもこの単位が必要という現状です。
頼りにするのがこの板だけというまわりもあてにならない状況で申し訳あり
ませんが、お付き合いいただけると幸いです。
先ほどの質問につきましては、いただいたアドバイスを元に選びます。
もうひとつだけお願いします。
質問 yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。
という質問です。
「代入」というテーマで授業した内容からだと思いますが、もう途中から
何言ってるのかわかりませんでした…。
すみませんが、よろしくお願いいたします。
407:１３２人目の素数さん
12/01/29 00:00:41.31
>>406
とりあえず言えることは、
>>397のような問題は通常、
「論理式の定義から作れるものはどれか？」ということが問うているので、
>>403のような定義から作れるか試してみろってことです。
＞質問 yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。
NOです。
束縛された変数には代入できないです。
※直感的理解
∃yP(y,a)：yは束縛されている、aは束縛されていない。
408:１３２人目の素数さん
12/01/29 00:18:37.92
407さん、ありがとうございます。
ちょっとわかったような気がします。
とすると、
∀xＰx⊃∀yＲ(x,y)において、freeに現れているxにzを
代入した論理式を書きなさい。
という問いに対しては、∀xＰx⊃∀yＲ(z,y)
と答えればよろしいのでしょうか。
もはやこんな感じ、という理解しかできませんが…。
409:１３２人目の素数さん
12/01/29 00:58:59.64
>>397
通常の形成規則にしたがえば、論理式(wff)である記号列は(2)だけで、(1),(3),(4)はwffsではない。
410:１３２人目の素数さん
12/01/29 05:19:36.48
うぇるふぉーむどふぉーみゅら
411:１３２人目の素数さん
12/01/29 07:11:11.50
圏論による数学の基礎について語ろう！
412:１３２人目の素数さん
12/01/29 08:33:10.32
上のほうで圏論と集合論（巨大基数）の関係が話題になってたけど、
圏論を他の代数構造同様に（クラスサイズっていう違いはあるが）集合論の中で実現して
っていう話だから数学の基礎としての圏論というのとはなんか違うな。
413:１３２人目の素数さん
12/01/29 10:23:59.82
>403だけ？∀に関する他のルールは無いの？
普通に考えれば∀zが入れ子になっている(4)が怪しいけど、
仲間外れというなら束縛したwの出て来ない(1)も怪しい。
414:１３２人目の素数さん
12/01/29 10:38:06.58
量化記号がダブるとか、∀zが入れ子になるとか、束縛したwが出て来ないとか
そんな理由で論理式にしないなんてことよくするの？
415:１３２人目の素数さん
12/01/29 11:04:29.57
>>414
とにかくあれは問題のための問題（悪問）と思う。
実際に使うために論理式を書く場合は、変数はダブらないように書くし、
中に出てこない変数を束縛するなんてこともしないだろ。
416:１３２人目の素数さん
12/01/29 11:08:55.44
そうだな。あんなことをやってるから教養は要らないってことになる。あれは文系かな？どうせ論理を教えるならもっと違うやりかたがあるがな。
417:１３２人目の素数さん
12/01/29 12:44:33.77
圏論上の形式的議論を圏論だけでできるんですか？
述語論理は当然のように使っているようにみえるんですが、これでは圏論は自立していないと
いうことにはならないのですか？
418:１３２人目の素数さん
12/01/29 13:06:57.12
集合論だって述語論理は使っている。
述語論理の上のレベル（というか非論理的公理）として、
集合論などのほかの「数学の基礎」から自立できているかが問題。
述語論理から独立させようなんて誰も考えてないよ。
419:１３２人目の素数さん
12/01/29 14:55:33.43
そうだけど、集合論におけるメタ数学的議論は集合論で形式的に扱う事が出来るけど
圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難があるし、
その全ての側面を扱うのは難しいと思う
420:１３２人目の素数さん
12/01/29 15:19:53.03
>圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難がある
慣れの問題でしかない、という説もある。そしてその説には一理ある。
421:１３２人目の素数さん
12/01/29 16:12:47.01
前にちらっと話題に出てきた STS (Structural Theory of Sets) は、
述語論理から独立させて、様相命題論理で集合論を記述しようという話。
つまり比喩的に左側が機械語側、右側がユーザー側として階層をまとめると、
>>412が圏論と巨大基数の話に関して言ったこと：
一階述語論理 － 集合論 － 各数学（圏論もこの一つ）
数学の基礎として圏論
一階述語論理 － 圏論 － 各数学
STSの目指すもの
様相命題論理 ー 集合論 － 各数学
422:１３２人目の素数さん
12/01/29 17:40:49.18
>>418
>述語論理から独立させようなんて誰も考えてないよ。
だったら圏論は述語論理の単なるマクロ集であって、共通の基盤言語だなんて言い方は
しないほうがよいのではないですか？
423:１３２人目の素数さん
12/01/29 17:53:39.66
>>412
こんなんあるでよ
URLﾘﾝｸ(www.math.ucla.edu)
RELATING FIRST-ORDER SET THEORIES AND ELEMENTARY TOPOSES
424:１３２人目の素数さん
12/01/29 18:07:13.66
>>422
なんか色々なことをごっちゃに理解しているように見受けられるな。
「圏論が数学の共通の基盤言語」というのは、
数学の色々な構造から共通の性質を抜き出すのに便利というプラグマティックな話であって
「圏論は数学の基礎として数学と述語論理の橋渡しとなる」というのとは
また別の話だと俺は理解しているのだが。
425:１３２人目の素数さん
12/01/29 18:30:21.14
いや、巷で「数学の基礎」と言われていることの中身を突き詰めれば
>>422の言うとおりマクロ集ということでしかないのでは？
もちろん、それは集合論が数学の基礎というときも同様だけど。
＞なんて言い方はしないほうがよいのではないですか？
「集合論が数学の基礎だ」とか「圏論が集合論に代わる基礎となり得る」とかというのは、
ある意味使い古された言い回し。ここの住人が言い出したことではないので、
こんなところで「その言い方はおかしい」と言っても始まらない。
426:１３２人目の素数さん
12/01/29 18:52:36.82
>>425
「数学の基礎」と「数学の共通の基盤言語」は同じ意味内容だと主張したいの？
427:１３２人目の素数さん
12/01/29 19:32:32.95
数学の共通言語はTEXだよ
428:１３２人目の素数さん
12/01/29 22:07:17.38
圏論は所詮モデル論なんだよ。しかし言語の本質はシンタックスだ。
だから圏論は、共通も何もそもそも言語ですらないんだよ。
同じことは集合論にも言える。
わかるかな。
429:１３２人目の素数さん
12/01/29 22:08:49.88
↑あふぉ
430:１３２人目の素数さん
12/01/29 22:41:02.09
シンタックスだのセマンティクスというのは
メタレベルからオブジェクトレベルをいじる場合の手段の区分。
一階述語論理 － 集合論or圏論 － 数学各論
という階層は、
オブジェクトレベル、メタレベル、メタメタレベルなどの
一つのレベルの中での話。
（オブジェクトレベルの一階述語論理は、
セマンティクスだろうとシンタクスだろうとメタレベルの数学各論の一つになる。）
一つのレベルの中でセマンティクスだのシンタクスだの言うのは無意味。
431:１３２人目の素数さん
12/01/29 22:58:00.44
>>430 ややこしいな
432:１３２人目の素数さん
12/01/29 23:04:50.75
基礎付けの話になると、最終的にどっかで循環にならざるをえないからな。
それを尤もらしい美辞麗句で隠したのが、メタレベルと対象レベルの分離、ともいえるわけだｗ
433:１３２人目の素数さん
12/01/29 23:54:17.46
>>430
なるほど。数理論理学を学ぶために最低限必要なセンスとして
＊シンタックスとセマンティクスが区別できること
＊オブジェクトレベルとメタレベルが区別できること
＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること
の３つを伺っていましたが、最後の区別がよく分かりました。
434:１３２人目の素数さん
12/01/30 00:02:11.87
＞＊シンタックスとセマンティクスが区別できること
＞＊オブジェクトレベルとメタレベルが区別できること
＞＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること
これ至言だな
435:１３２人目の素数さん
12/01/30 00:18:37.06
シンタックスとセマンティックがはじめに理解すれば良い
メタな視点は後から考えれば良いし、ロジック学習の基礎において必須でもない。
436:１３２人目の素数さん
12/01/30 00:19:16.47
ソースは誰？ぐぐったら鴨さんのはてなが出てきたけど、これが初出？
437:１３２人目の素数さん
12/01/30 00:23:44.56
俺様勉強法を語って自分の無理解をひけらかしちまう馬鹿＝435、哀れだなｗｗ
438:１３２人目の素数さん
12/01/30 00:36:52.08
>>430で言われているように、
シンタックス（構文論）もセマンティクス（モデル論）もどちらもメタ的な視点の話なので、
良い子の皆さんは435のいうことを真に受けてはいけませんよ
439:１３２人目の素数さん
12/01/30 00:48:22.65
そんなことより、圏論による基礎の話はどうなった？
>>423のリンク先の論文の評価を聞きたい。
440:１３２人目の素数さん
12/01/30 05:32:38.82
>>432
ともいえる、なんて控えめである必要はなく、そう断言してしまってもいいと思う
というか「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」なんて
基礎付けの本質を突いた至言だと思う、鴨さんの３つの区別と並んで。
441:435
12/01/30 07:17:42.79
はじめはメタな視点を意識する必要がないという話しだが。
>>438の考えを認めるとすべての数学はメタな視点に基いている。
メタを意識する必要が出てくるのは不完全性定理や内部モデルから。
442:１３２人目の素数さん
12/01/30 07:40:09.73
435=441 のいうことが正しい。
430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
思っている人がありが、無限連鎖に陥るだけで、意味を考えることができ
ない。
443:１３２人目の素数さん
12/01/30 09:06:38.39
学部教養レベルの確認が一段落したら、圏論によってシンタックスとセマンティックスの
区別がなくなるという話もしようぜ。
444:名無しさん
12/01/30 18:58:02.88 Nob3XfwW
ちょうど話題が出たんで、甲鳥さんのページで質問です。
URLﾘﾝｸ(taurus.ics.nara-wu.ac.jp)
＞著者は、また、自然数論は完全性定理が成り立つには強すぎる体系である旨の
＞主張もしている。それも大違いである（こちらは、かなり広まっている誤解だ
＞が、どんなに広まっていようと、専門家に一言相談すれば「それは間違ってい
＞る」と言ってもらえるのだから、言い訳にはならない）。一階ペアノ算術（自
＞然数の加減乗除と大小比較ができて数学的帰納法が自由に使えるが、関数一般
＞や集合一般を自由に扱うことはできない世界と思って、ほぼ間違いない）は一
＞階述語論理上の公理系なので、完全性定理が適用できる。したがって、一階ペ
＞アノ算術の公理系から証明可能な式全体と、一階ペアノ算術の公理系が真とな
＞るすべての解釈で真となる式全体は、一致する。これを、「一階ペアノ算術は、
＞一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」という。
という部分ですが、
「一階ペアノ算術は、一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」
というのは本当に成り立つんでしょうか？今一書いてあることが理解できないのですが。
445:名無しさん
12/01/30 19:03:08.17 qQ0NhdK4
>>444
もちろん本当だと思うが、どう理解できないの？
446:444
12/01/30 19:44:03.54
あぁ勘違いしていた。
完全性定理は論理だけに関する定理だった。
447:名無しさん
12/01/30 20:09:26.65 ZFRpVEeB
>>443
こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
448:444
12/01/30 20:37:41.38
林さんの数理論理学では
述語論理の完全性と古典算術の完全性を別の定理として区別していますね。（独言
449:名無しさん
12/01/30 20:58:41.96 qQ0NhdK4
>>447 駆け出しだな
450:名無しさん
12/01/30 21:05:58.07
＞圏論によってシンタックスとセマンティックスの区別がなくなる
別にそんなこと無いですけど……
と書こうと思ったら既出だった
451:名無しさん
12/01/31 05:56:45.85
専門家をバカにできるとは 441=442 はアスペか？隔離スレからでてくんな。
452:435
12/01/31 07:13:02.56
どうでもいいことだが、>>442は別人。
453:名無しさん
12/01/31 07:35:35.85
>397 Ｌｐの論理式でないのはどれか。
(1)∀w∀x∃zＲ(x,z)
(2)∀xＰx⊃∀xＲ(x,c)
(3)∀xＰx⊃∀cＲ(x,c)
(4)∀z∀x(∀xＰx⊃∀zＲ(zz))
コピペなら明瞭に(4) R(zz) はwww
誤植でR(z,z)にしても「R(z)三R(z,z)」は未だ証明されてない
よーするに ここでの単位は とらぬのが正解
あふぉ が伝染って 後遺症で困るとおも晴れri
454:名無しさん
12/01/31 07:46:24.58
どうも本当にアスペが隔離スレから出てきたようだな
455:名無しさん
12/01/31 10:16:28.28
>>441
通常の数学（特に代数構造など）の話でも、
★そういう見方をすれば★メタ的な視点に立っているものが多い、
ということに気づけないようでは数理論理学のお先真っ暗。
456:名無しさん
12/01/31 18:12:14.65
とりあえず宣言しとくけど
今夜0時までに
田中の数学基礎論講義の5章までの定理をすべて
Coqで証明するよ＾＾
457:名無しさん
12/01/31 19:23:22.88
すげえ！
458:名無しさん
12/01/31 23:52:26.53
Definition P1(a b:Prop):Prop:=
a->(b->a).
Definition P2(a b c:Prop):Prop:=
(a->(b->c))->((a->b)->(a->c)).
Definition P3(a b:Prop):Prop:=
(~b->~a)->(a->b).
今日はここらへんまでかな。
459:名無しさん
12/02/01 09:29:56.50 S/Q8pgaI
スレの勢いからして
もうそろそろ次スレの季節だな
460:１３２人目の素数さん
12/02/02 00:08:01.24
Record L_PA:Type:=
language
(Func:Set)
(Rela:Set)
(arity:Func+Rela->nat).
今夜はここまで
461:１３２人目の素数さん
12/02/02 04:30:22.70
＞430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
＞思っている人がありが、無限連鎖に陥るだけで、意味を考えることができない。
馬の耳に念仏だな、こりゃ。念仏の「こころ」がまるで分かっちゃない。
馬＝442
念仏＝「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」
462:１３２人目の素数さん
12/02/02 05:28:18.34
圏論話は終了か？
463:１３２人目の素数さん
12/02/02 07:31:16.88
┌∩┐(◣_◢)┌∩┐
上の方にある、
一階述語論理 － 集合論 － 各数学
の図式は古典的で、考えているのは数学屋だけ。
実際には一階述語論理 － 集合論の間の区別は曖昧。
464:１３２人目の素数さん
12/02/02 11:50:41.14
参考文献を上げて下さい
465:１３２人目の素数さん
12/02/02 18:25:33.46
┌∩┐(◣_◢)┌∩┐
この本にZFCを一階論理で厳密に展開しているので参考にすること。
Axiomatic Set Theory (Graduate Texts in Mathematics) [Paperback]
Gaisi Takeuti (Author), Wilson M. Zaring (Author)
URLﾘﾝｸ(www.amazon.com)
466:１３２人目の素数さん
12/02/02 18:32:31.58
>>423
（圏論的意味での）イデアル全体とか取っているのは、
そのトポスが集合論の世界に含まれている前提での話。
「一階述語論理と数学をつなぐ」という意味での
「基礎としての圏論」の研究とは言いがたい。
467:１３２人目の素数さん
12/02/02 19:58:10.03
463が言ってる集合論ってまさか
「集合と位相」で習うようなことじゃないだろうか
468:１３２人目の素数さん
12/02/02 20:43:10.06
>>467 だから言っただろ。駆け出しがうようよしてんだよ
469:１３２人目の素数さん
12/02/02 21:34:56.20
┌∩┐(◣_◢)┌∩┐
一階述語論理の言語にZFCの公理系を添加したものと∈-モデルからなる数学は、
厳密に分離することが出来ない、これは実際に展開してみないと気付きにくい。
例えばキューネンなどの本では述語論理の箇所が省略されているので気付けない。
>>465の本の冒頭が参考になる。
470:１３２人目の素数さん
12/02/02 22:25:47.07
「∈-モデルからなる数学」って何のこと言ってるの？
そもそも>>469では述語論理＋ZFCとその上の数学とを
厳密に区別できないと言っているのに対して
>>463では述語論理と集合論（ZFC）とは区別できないと
少し別のことを言っているように思うんだが
集合論は数学をやる上での基本的な言葉みたいなものだから
基本的な論理と一体だとか言うのは普通の数学やってる人達で、
却って情報系・哲学系の人とか数学でもロジックやってる人は
集合論（ZFC）の公理と述語論理の公理は別のレベルのものだとして明確に区別すると思う
（一部の新論理主義の立場に立つ哲学者等を除く）
471:１３２人目の素数さん
12/02/03 04:35:23.02
他人には意味不明な用語法を断りなしにするのは、トンデモか駆け出しの証拠ｗ
472:１３２人目の素数さん
12/02/03 06:24:32.83
>>463
等号公理は、一階述語論理の公理なのか、集合論の公理なのかはっきりしない、
とかそういう意味で区別が曖昧と言っているのかな？
それはイエメンとサウジアラビアの国境が未画定（つまり曖昧）だから
国家としてのイエメンとサウジアラビアの区別が厳密に区別できない
と言っているようなもので的外れ。
473:１３２人目の素数さん
12/02/03 07:11:59.26
>>466
確かにイデヤールの部分はそうなんだけど、
かなりの部分は一階述語論理の直上のものとして理解できるでしょ、
elementary topos というのは正にそれ故に意義のある概念。
集合論に依存していいのなら Grothendieck topos で十分だった。
その論文では「canonical injection である」という述語が、
集合論と同じ表現力を持たせる為に圏論側で必要な「述語記号」だと言ってる。
とはいえ、集合論に依存している部分とそうでない部分をごちゃ混ぜにしているのは確かに問題。
圏論による基礎を標榜している指導的な研究者である著者達がこんな書き方をするから、
「圏論は集合論に変わる基礎」と言っても
一階述語論理 － 集合論 － 圏論 － 各数学
みたいに「屋上屋を重ねる」ような無駄なこと、っていう印象を持たれてしまう。
474:１３２人目の素数さん
12/02/03 07:21:18.20
┌∩┐(◣_◢)┌∩┐
Oh,Motherfucker!（＾＾；
等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。
475:１３２人目の素数さん
12/02/03 07:25:41.91
問、等号なし一階述語論理でZFC外延公理から以下を導け：
∀x(x∈a ⇔ x∈b) ⇒ (a∈c ⇔ b∈c)
476:１３２人目の素数さん
12/02/03 08:05:16.63
＞等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。
こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
477:１３２人目の素数さん
12/02/03 10:06:55.24
>>473
>みたいに「屋上屋を重ねる」ような無駄なこと
それ以前に、圏論が述語論理（λhol含む）や集合論のような共通言語には到底なりえんのじゃないかな。
言語（道具）にしては難しすぎるし奇妙すぎる。
478:１３２人目の素数さん
12/02/03 16:04:59.16
>述語論理（λhol含む）や集合論のような共通言語
述語論理上の理論である集合論と述語論理を並列な言語としてる時点でアウト！
479:１３２人目の素数さん
12/02/03 17:27:53.50
>等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれる
「等号なし」とは、等号記号が言語に入っていないのか、記号はあるが等号公理が入っていないのか。
中身以前に、自分の発言に必要な情報が欠けていて多義的であることに気づかないってのは、やっぱり駆け出しの証拠だ。
謙虚に勉強しなおすがよろしかろう。
ちなみに、前者だとすると、標準的な外延性公理がそもそも記述できない。
後者ならば>>475の言う通り。どちらにしてもおかしい。
480:１３２人目の素数さん
12/02/03 18:12:32.14
>>478 あんたもそういう区別がやっとできるようになった駆け出しだな。
もっと大事なことを言えよ。
481:１３２人目の素数さん
12/02/03 19:14:49.34
欠けた情報は集合論という言葉に対してもそう。
一階述語論理上のZFC⇒集合論だが逆は成り立たん。
482:１３２人目の素数さん
12/02/03 19:39:41.34
┌∩┐(◣_◢)┌∩┐
Suck me!
等号公理を抜いた一階述語論理。
こいつさんに2項述語＝をぶち込むさかい。
483:１３２人目の素数さん
12/02/04 00:23:06.52
Require Import Classical_Pred_Type.
Section Generic.
Variable U:Set.
Require Export Le.
Require Export Lt.
Require Export Plus.
Require Export Gt.
Require Export Minus.
Require Export Mult.
Require Export Between.
Require Export Peano_dec.
Require Export Compare_dec.
Require Export Factorial.
Require Export EqNat.
Require Export Wf_nat.
Require Import Decidable.
Goal forall n, n<=n.
Goal forall n, n<=n->n<=n.
Goal forall n m, n<=m->m<=n.
Goal forall n m, n<m->m<n.
Goal U=U.
Goal exists n,n<n.
Theorem A0:forall(a b c:nat),a=b->a=c.
Proof.
intros.
先ずは準備っと。
484:１３２人目の素数さん
12/02/04 02:08:35.82
>>473
「数学の基礎としての○○論」の研究なんてのはきょうび流行らない。
元祖の集合論でも、数学の基礎としての集合論の研究なんて久しく聞かないね。
485:１３２人目の素数さん
12/02/04 04:09:04.46
482を恥の上塗りというのだなｗｗｗ
486:１３２人目の素数さん
12/02/04 05:08:41.52
>>485
同感。
ところでmother fuckerの┌∩┐(◣_◢)┌∩┐って
馬鹿さ加減というか無知さ加減が以前の「考える人」と良く似てると思うのだが。
487:１３２人目の素数さん
12/02/04 06:18:45.27
>>484
確かに。部外者が想像する集合論と、実際に集合論で研究されている内容には差異があるかも。
数学の基礎として集合論を志すと、研究の現場に行ってみると
「こういうことをやりたかったのではない！」と思うだろうな。
たしかに専門分野としての集合論は「集合というものの性質を定める規約集」ではなく「累積階層という対象の構造を探求する研究」になっていますね。
とはキューネン本の訳者の言。
488:１３２人目の素数さん
12/02/04 06:47:41.58
>>486
禿堂
489:１３２人目の素数さん
12/02/04 09:32:19.48
(*鶏慣れのために算術命題をチェック。*)
Goal forall (n m : nat)(f : nat -> nat), (S n = S m) -> n = m->f n = n -> S (f (f n)) = S m -> n = m.
intros.
rewrite H1 in H2.
rewrite H1 in H2.
apply H0.
Qed.
490:１３２人目の素数さん
12/02/04 11:17:47.41
スレチですまんのだけど、Coqだと
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x.
という風に等号を定義するだけで（ちなみに上記の意味は、「Type Aの変数xに対して
x=x（eq A x xのこと）の証明が存在することを仮定し、その証明をeq_reflと名づける」といった感じ。）
eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, eq A x y -> P y
というような等号公理が導かれてしまうけど、これってどういう原理なの？
わかりやすい説明とか文献あったら教えてくだされ。エラいひと！
491:１３２人目の素数さん
12/02/04 12:25:40.34
>>481
欠けた情報：⇒の意味
怪しげな記号の使い方をするのもトンデモや駆け出しの証拠ｗ
492:１３２人目の素数さん
12/02/04 13:27:08.40
>>473
>かなりの部分は一階述語論理の直上のものとして理解できる
とすると、ZFC その他一階述語理論としての集合論と同じく、
一階述語理論としての圏論がある筈だけど、そんなん聞いたことないぞ
493:１３２人目の素数さん
12/02/04 13:34:28.50
>>491
それはつまらん言い掛かりにしか見えない
494:１３２人目の素数さん
12/02/04 18:53:42.74
>>491
いや、言いがかりではなく481は何を言いたいのか分からん。
自分で読み返してみてそれに気づけないのなら真性駆け出し。
玄人に質問の意図を伝えられない素人の図、だなｗｗ
495:１３２人目の素数さん
12/02/04 19:14:08.17
Awodeyの教科書に
集合論は数学の基礎だというのと
圏論は数学の基礎だというのは意味合いが違うよ的な話が書いてあるよ