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の教科書に
集合論は数学の基礎だというのと
圏論は数学の基礎だというのは意味合いが違うよ的な話が書いてあるよ
496:１３２人目の素数さん
12/02/04 19:19:34.73
こういうのこそ2chらしくていい
俺は「真性」は大歓迎よ
もっと自己主張してほしい
497:１３２人目の素数さん
12/02/04 19:36:05.78
「集合論の公理系」と「ZFC（＋追加公理）」は
イコールじゃないよというようなことを言いたいんだろうけど、
handbook of set theoryとかJechとかは
事実上ZFCかその保守拡大のBGのことしか書いてないよ
良くてMKにちょっと言及するくらい
498:１３２人目の素数さん
12/02/04 19:41:01.53
結局、「⇒」で何を言おうとしているのかが分からないことが原因。
499:１３２人目の素数さん
12/02/04 19:53:43.05
多分
一階述語論理にZFCの公理を加えることだけが
集合を展開する唯一の手段ではない、という趣旨かと。
500:１３２人目の素数さん
12/02/04 20:42:18.03
>>495
定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
「集合論は数学の基礎」というのも、Simpson 的な意味で言われる場合もあって、
Awodey が彼の本で言及しているような意味とは必ずしもならない。
結局のところ、言われている文脈を考慮しなければ、どういう意味かは分からない。
しかし「ひねっていない」言葉の意味、というか伝統的なオーソドックスな意味というのがあって、
特に断り書きがないような場合には暗黙の了解的にその意味で理解すべき、というのがある。
それが「数学各論と一階述語論理を繋ぐ」という意味だし、
これがオーソドックスだからこと Awodey が対比の為に言及している。
（オーソドックスでなければわざわざ対比に使わない。）
このオーソドックスな意味での「圏論による基礎」は、
オーソドックスなだけにかなり長いこと研究されている。
いまどき流行らないというのは認めざるを得ないところだが。
501:１３２人目の素数さん
12/02/04 20:53:10.81
>>492
Elementary topos は、確かにモデルに関して記述される場合が多いけれど、
object と morphism の２つの sort を持つ一階述語論理
（お好みなら identity を使って morphism だけの方法でもいいが）を考え、
identity と composition を関数記号として入れれば、
elementary topos であることを一階述語論理で記述できる。
元々 "elementary" という言葉は、
elementary extension, elementary submodel 等々、
一階述語論理の観点という意味合いを持つ。
トポスの重要な性質をすべて
（上述の言語による）一階述語論理で記述できた、
というのが elementary topos の意義。
公理系に関する研究がないじゃないか、というかも知れないが：
完全性があるのだから、
そうやって記述された elementary topos の公理系で何が証明できるか調べることと、
elementary topos に共通する("elementary" な)性質を調べることは同値。
502:１３２人目の素数さん
12/02/04 20:54:57.50
誤字訂正：
×これがオーソドックスだからこと Awodey が対比の為に言及している。
○これがオーソドックスだからこそ Awodey が対比の為に言及している。
503:１３２人目の素数さん
12/02/04 21:27:37.21
>>501
勉強になる
>トポスの重要な性質をすべて（上述の言語による）一階述語論理で記述できた
これはFOLの記述力から自明じゃないかと思うんだが？
504:１３２人目の素数さん
12/02/04 23:06:32.52
>>503
FOLの記述力に関するどういう定理から自明なんだい？
Lawvere が elementary topos の概念を出す前には、
トポスというのは「層全体のなす構造」って定義しかなかったんだよ？
505:１３２人目の素数さん
12/02/04 23:22:32.52
＞定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
＞他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
基礎と言ったらヒルベルトプログラムでの意味しか考えられない単細胞なアスペに聞かしてやりたい。
と思ったらいま自分の隔離スレで活動始めやがったとこだった。
ということはこのレスも読んでいるに違いない。
506:１３２人目の素数さん
12/02/04 23:38:56.73
500だけど、>>505に補足：
「数学の基礎」の一番オーソドックスな伝統的な意味は、
Hilbert Programme の意味での基礎付けね。
でも、アスペに言われるまでもなく、
それが数学的に不可能なのことは既に分かっているので、
それ以降は（数学史の文脈などを除けば）
オーソドックスな意味は500で言った通りってこと。
507:? ＊＊論研究報告
12/02/04 23:50:11.10
＊＊論数学では虚数 i=√-1 はある質（表現）からそれと異なった質（表現）
に移る演算単位である。すると空間の距離Ｘとそれと直角な距離Ｙは
異なった質の関係にあります。からｒ＝Ｘ＋Ｙｉです。ＹiやＸの表現を
消すと当然存在量が残ります。消滅表現をＡ＾*と表すとＸ・Ｘ＾2＝Ｘ＾２
（Ｙｉ）・（Ｙｉ）＾*＝Ｙ＾２でありｒ＾２＝Ｘ＾２＋Ｙ＾で
ピタゴラスの定理です。
9 ：? ＊＊論研究報告：2012/02/01(水) 01:09:12.22 ID:2eW/+tej
おっと間違えた。Ｘ・Ｘ＾2＝Ｘ＾２ ではなくて
Ｘ・Ｘ＾*＝Ｘ＾２です。
10 ：? ＊＊論研究報告：2012/02/01(水) 01:15:30.41 ID:2eW/+tej
虚数の意味は前から言っているんだが
未だに数学会では遅れた考えを外国でもやっていて
未だ＊＊論には追い付いていない。これは人類の
知的衰退と思われる。我が新人類右脳同盟の啓蒙が
必要と思われる。長年の物質欲ボケがたたってると
思われる。身を引き締めよ。
508:１３２人目の素数さん
12/02/05 00:10:26.39
>>497
確かに「専門分野としての集合論」では、ZFC に公理を加えたものばかりしか考えませんね。
仰る通り、たまにBGとかMKとか出てきますけど。
古典的な数学は殆ど展開できると言われている KP (kripke-Platek 集合論)や
圏論と関係が深い MacLane 集合論や Lawvere 集合論、
直観主義論理の数学は殆ど展開できると言われる CZF (Constructiv ZF)、
某所で話題沸騰中の Quine の NF (New Foundation)などなどの
「その他の集合論」は、集合論というより証明論で研究されているって印象。
「集合というものの性質を定める規約集」を志す人は、集合論じゃなくて証明論に行くべきだな。
509:スレタイスレ446
12/02/05 00:23:04.68
>>490
スレチじゃないと思いますね。
Coqはバージョンによって多少違うようですが、
シンタックスはCIC（帰納的構成計算）という型言語で出来ています。
Coqは帰納的な定理から型理論の導出規則に基づいて、
自動的に新たな定理を作る機能があります、等号公理以外についても。
URLﾘﾝｸ(www3.di.uminho.pt)
の23ページ位からですね。
510:１３２人目の素数さん
12/02/05 00:46:34.99
お、スレ主がお帰りになられたか
511:１３２人目の素数さん
12/02/05 00:59:14.15
C.C. Chang , H. Jerome Keisler
Model Theory: Third Edition がDoverで出るか。
512:１３２人目の素数さん
12/02/05 02:06:56.09
「駆け出し」って煽り文句が流行ってるようだな。
513:１３２人目の素数さん
12/02/05 05:30:41.05
>>501
そうやって一階述語論理上の理論としての圏論は考えられるのは事実だけど、
そういうのがあまり出てこないのは別の理由からじゃないか？
圏論と型理論（高階算術ともいう）との間にかなり密接な関係があることは
かなり早い段階で分かっていた。
(Lambek & Scott の Introduction to Higher Order Categorical Logic など参照。)
型理論は、圏論云々よりはるか前からある「数学の基礎」候補だった。
だから圏論に合わせた一階述語理論をわざわざ作るまでもなく、
型理論を「圏論による基礎のための一階述語理論」として研究されてきたのだと
俺は理解しているがどうか。
514:１３２人目の素数さん
12/02/05 06:37:46.43
いつものことながら圏論基礎ネタは盛り上がるのう
駆け出しから玄人まで一言いいたくなるテーマなんだろうな
515:１３２人目の素数さん
12/02/05 10:35:20.26
>>514
というか、裸の王様のニオイがするからじゃないかな？
516:１３２人目の素数さん
12/02/05 15:25:59.50
集合論は数学の基礎だと言い出したのは
HilbertじゃなくてBourbakiだと思うけど。
集合論はとても超越性の高い理論だから
Hilbertとかは、とても数学全体の基礎にはなりにくいという感覚をまだ持ってたんじゃないかな
517:１３２人目の素数さん
12/02/05 18:18:25.21
>>516
集合論が数学の基礎だというのはまあ違和感はない。
述語論理上の最小限の言語だろう。
その点圏論はまったく違う。いろんな怪しげな概念を強制してくる。
518:１３２人目の素数さん
12/02/05 19:04:10.61
圏論の概念が怪しげだと思うのは、メタな思考に慣れてないからでは？
519:１３２人目の素数さん
12/02/05 19:17:41.18
>>517
圏論が各数学と一階述語論理と繋げるという意味で基礎となりうるかかどうかは既に技術的な問題になっている。
違和感があろうがなかろうがそういう主観的なものはもはや関係ない。
ま、流行るかどうかは主観的な問題も込みなので、知らんけどな。
520:１３２人目の素数さん
12/02/05 19:50:34.43
>集合論が数学の基礎だというのはまあ違和感はない。
>述語論理上の最小限の言語だろう。
どういう意味で最小限と言っているの？
集合論より大きくない述語論理の言語は存在するのだから最小ではないと思うけど？
521:１３２人目の素数さん
12/02/05 20:09:38.23
言語の大小なんて、公理の数を数えるのと同じでナンセンスだろ。
（二つの公理も連言で繋げば一つになるように）
ちょっとした小細工で本質的に変わらないのに大きくも小さくもできる。
522:１３２人目の素数さん
12/02/05 20:14:19.87
>>518
メタなのはむしろ望ましいが、そのメタレベルの概念が怪しげに見えると言っている。
圏論の独自性（の一つ）は、まさにそういう理論の怪しさや不格好のようなことを見抜ける
ところにあるのかなと思っていたんだ。
>>519
言葉はちょっと違うが、流行るかどうかがやっぱり最も大事じゃないの？
技術的に詰めているものが望遠鏡なのか単なるガラスなのか
523:１３２人目の素数さん
12/02/05 20:23:13.33
なんか「ユークリッド幾何は違和感はない、射影幾何は違和感がある」と同レベルに見えるんだよね。
確かに非ユークリッド幾何は、ユークリッド幾何ほどは流行らない。
しかし非ユークリッド幾何には非ユークリッド幾何にしかない意義がある。
両者の比較や、目的による使い分けなどをすることによる相乗効果で幾何学がより深化することになった。
集合論による数学の基礎と圏論による数学の基礎も同じではないのかな？
両方あることで、数学の形式化の理解を深化させてくれる。
524:１３２人目の素数さん
12/02/05 20:33:54.72
優等生の模範解答ですな
525:１３２人目の素数さん
12/02/05 20:39:05.54
射影幾何は非ユークリッド幾何ではないけどね
526:１３２人目の素数さん
12/02/05 20:42:59.35
>>523
紳士的な議論だが、
集合論もあるけどこれもある。流行らないかもしれないが、あったらあったで
いいじゃないか、なんていう圏論は嫌でしょ。
>>520
∈だけ追加だよね？たしか
極小といえばよかったかな
>>521
そんなことはない
527:１３２人目の素数さん
12/02/05 20:50:02.47
>...なんていう圏論は嫌でしょ。
いや、君が嫌ならそれでいいんじゃない？
でも他人に嫌がるように強制できないことも分かるでしょ。
つーか、議論のレベルを女子高生みたいな好き嫌いレベルまで落とすんなら
っこでは誰も君との議論に付き合わなくなると思うけどね。
528:１３２人目の素数さん
12/02/05 20:59:27.54
＞>>521
＞そんなことはない
それだけだと>>527で批判されている「嫌でしょ」と同じく全く説得力ないんだが？
どう「そんなことはない」のか説明してくれないと反論のしようがない。
529:１３２人目の素数さん
12/02/05 21:09:49.50
どんな言語でも、述語記号・関数記号・定数記号が全部有限なら、
小細工することで極小な言語にすることが出来ますね。
公理が極小というのが無意味なのと一緒。最小は勿論無理ですが。
530:490
12/02/05 21:17:56.23
>>509
情報ありがとうございます。参考になりました。他にもなにか文献等
ご紹介いただけないでしょうか。
531:１３２人目の素数さん
12/02/05 21:21:15.51
何を言っているのかさっぱり分かんない…
ちょっと気まぐれで覗いてみたが、まるで地獄だ…
532:１３２人目の素数さん
12/02/05 21:24:59.11
>>522
>流行るかどうかがやっぱり最も大事じゃないの？
そもそも基礎論自体が流行っていないｗｗ
集合論が圏論より流行ってると言っても団栗の背比べｗｗｗ
533:１３２人目の素数さん
12/02/05 21:42:26.99
>>527
へたに柔らかく言い過ぎたか？
そんな圏論ならそんなふうにニッチにやっていけばいい。
だが圏論にはもっと大きな意味があると聞こえているので、もしそうなら衆人にそれが分かるように
言ってくれと言った。
>>528
だって公理の数の件は数えるものが悪いだけだね？
それくらいあなたにも分かっているだろと思うから。
>>529
528とも同じくいまは本質的なことじゃないと思うのでごめん。
534:スレタイスレ446
12/02/05 21:46:45.82
>>530
URLﾘﾝｸ(citeseerx.ist.psu.edu)
私に探せるものであなたに探せないものはない。
535:１３２人目の素数さん
12/02/05 21:58:06.95
＞圏論にはもっと大きな意味があると聞こえているので
こういう誤解をする人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
536:スレタイスレ446
12/02/05 22:01:36.30
URLﾘﾝｸ(www.springerlink.com)
>>530
申し訳ないが読んだことがない本で・・・。
537:１３２人目の素数さん
12/02/05 22:10:19.25
>>533
>そんな圏論ならそんなふうにニッチにやっていけばいい。
そんなふうがニッチと思うかどうかは結局主観の問題だからね。
「集合論の問題はニッチなものだけじゃない」と何人かの専門家が解説しているのを見てきたけど、
ほとんどの部外者には「なんだ、やっぱりニッチな話じゃん」としか思わないだろうし。
ニッチかどうかなんてそんなもんよ。
538:１３２人目の素数さん
12/02/05 22:14:10.18
>535 これは必ずしも誤解ではなく、たしかに昔からよく耳にするな
539:１３２人目の素数さん
12/02/05 22:20:50.39
>>537
客観性のない主観的な罵り言葉なんて、負け惜しみの捨て台詞なんだから生暖かくスルーしてやればよろし。
540:１３２人目の素数さん
12/02/05 22:32:07.80
>>538
「もっと大きな意味」とか曖昧な言葉を含んでいるものに
「誤解ではなく」とか断言できる神経が全く理解できないな。
541:１３２人目の素数さん
12/02/05 22:40:37.13
>>540
まさか圏論の近くにはこんな人が多いんじゃないだろなｗ
542:１３２人目の素数さん
12/02/05 22:48:13.06
低俗な煽り合いはもう終了でいい？
もっと生産的な話がしたくてさっきから待ってるんだけど。
>>513
圏論に対応させる形式体系として型理論の方がよく出てくるのは確かにそおの通り。
だけど、圏論をそのまま一階述語論理にのっける公理系も Lwavere を始め研究されている。
最近でも以下のような論文が出ている。最近つっても10年以上前だけど。
URLﾘﾝｸ(www.cwru.edu)
543:１３２人目の素数さん
12/02/05 23:06:11.24
>538,541
そこまで言うのなら「よく耳にする」で済ませないで、
出典を明らかにするなりリンク貼るなりすれば？
そうすれば「低俗な煽り合い」と言われないで済むと思うけど。
544:１３２人目の素数さん
12/02/05 23:41:57.51
>>529
A∧BよりAの方が短い、という意味では公理系の極小性は定義できない？
もちろん、Aと全然違うCとどちらが小さいとも言えないから
集合論と圏論の比較には役に立たないだろうけどさ。
545:１３２人目の素数さん
12/02/06 01:01:17.41
>>526,>>533
数学の基礎付け・形式化に、集合論は必須のものなのか、
それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか、
という問題は重要な問題だと思う。
だから「集合論もあるけどこれもある」っていう圏論の研究は意味があるし、全くニッチな研究だとは思わない。
数学の基礎付け・形式化そのものがニッチだという人には「興味が違うのね」としか言えないけど。
546:１３２人目の素数さん
12/02/06 01:17:56.40
哲オタ乙。研究にどんな意味があるかどうかなんて言い方次第って実例だなｗ
547:１３２人目の素数さん
12/02/06 02:25:02.65
538が言っているのは
「独立した個を重視する西洋近代の終焉が...、これからは関係性を重視した圏論が...」
っていうポモな人たち（いや本当にポモなのかも知らないけど）の発言なんじゃない？
そんなのに踊らされてるなんて...
548:１３２人目の素数さん
12/02/06 03:56:14.39
>>544
＞数学の基礎付け・形式化に、集合論は必須のものなのか、
＞それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか
その大事な大事な研究の結果、どっちだと分かったの？少なくとも結論には興味ある。
549:１３２人目の素数さん
12/02/06 06:32:36.80
>>548
横レスかもしらんが、型理論型理論と言ってるように、
型理論で形式化できるものは圏論を使って形式化できる。
「通常の数学」はこの範囲。しかし「通常ではない数学」が問題。
集合論でも圏論が形式化できるかが色々微妙なように、
逆に圏論での形式化では集合論的な数学が問題になる。
特に置換公理が型理論（よって圏論）とは相性が悪いので、
このスレか関連スレでも何度か話題になっているように
置換公理を使った数学（要するに集合論的な数学）をどう評価するべきかという問題になる。