- DaiskeIkegami
- 5091
- 0
- 3
- 0
たぶんsubobject classifierが圏の言葉でinternal Hilbert sp. obj. みたいなことになっていなければなるまい、想像もつかぬ
2013-03-03 15:18:51@srb_2 初めまして。カリフォルニアで集合論やっている池上と申します。突然ですがコメントさせてもらいます。
2013-03-03 15:30:11@srb_2 強制法やウルトラパワーを grothendieck topology とそれ上の sheaf を使って表現する,という話があって,強制法の方は McLane と Moerdijk の "Sheaves in geometry and logic" に載ってます:
2013-03-03 15:32:56@srb_2 ウルトラパワーの方は,佐藤憲太郎さんのという方の修士論文で見ましたが,他の reference はちょっとわかりません。
2013-03-03 15:34:14@srb_2 あとは,sheaf semantics というやつがあって,直感主義において sound かつ complete になるそうですが,僕はちょっと詳しくないので,どの reference がいいかはちょっとわかりません。
2013-03-03 15:36:03@srb_2 一般のトポスから始めて semantics を与える,という話は僕は聞いたことはありませんが,あるのかもしれないですね。
2013-03-03 15:38:58@srb_2 オランダの Moerdijk なんかはこの辺詳しそうですが,日本人だと,スイスにいる(?)佐藤憲太郎さん,オックスフォードにいる丸山善宏さんあたりが詳しそうなので,興味があったら聞いてみてはいかがでしょうか?
2013-03-03 15:41:11@DaiskeIkegami はい、初めまして、宮崎と申します。コメントありがとうございます。紹介頂いたMacLaneの本を今読んでいて、トポスと強制法の関連を念頭においた発言でした。
2013-03-03 15:38:44@srb_2 そうですか。僕は強制法の部分は読んでないので有益なコメントはあまりできませんが,佐藤さんの話を聞いていたときは,以下のような感じでした:
2013-03-03 15:43:16@srb_2 poset P, p in P, A subset P が与えられたとき,「A が p を cover する」というのは A が dense below p で定義して,poset P を普通に圏と見るとグロタンディーク位相の構造が入ります。
2013-03-03 15:46:34@srb_2 あ,もしもう強制法の章を読んでらしたらこのコメントは無意味だと思うので,言ってもらえると助かります。
2013-03-03 15:50:18@srb_2 で,ここから少し曖昧になりますが,theory T に対し,theory T を満たすモデルの圏,というのを考えます。ここでいうモデルは古典論理の構造でなくて,もっと一般的な非古典論理の構造になってます。
2013-03-03 16:06:12@srb_2 で,その圏を Mod (T) で表したとき,先程のグロタンディーク位相上の Mod(T) に値をとる sheaf を,各 p in P ごとに P-name 全体と "p forces phi (sigma)" という関係の組をモデルと見て,導入します。
2013-03-03 16:09:04@srb_2 ここまでは,generic filter を取らずに全部 ground model で書けていて,強制法の文脈では "syntactical" な部分です。
2013-03-03 16:10:37@srb_2 で,佐藤さんの論文では,点に対応する概念として stalker というものを導入していて,上のグロタンディーク以上では V-generic filter に一致するもので,そこで上の sheaf の stalk を取ったものが強制拡大になってます。
2013-03-03 16:12:45@srb_2 このグロタンディーク位相に関しては,stalker の概念と geometric point のそれは一致すると思うのですが,ちょっと自信がありません。
2013-03-03 16:14:55@srb_2 佐藤さんの論文では,無限基数 κ に対して "almost kappa-covering topology" というグロタンディーク位相を導入して,κ 上の measure を stalker と見てウルトラパワーも表現しています。
2013-03-03 16:16:38@srb_2 generic ultrapower や symmetric model とかもこういう感じで表現できるみたいです。
2013-03-03 16:18:54@srb_2 この研究は,強制法・ウルトラパワーと全く違うモデルの作り方を探すうえで非常に興味深いんですけど,今のところそういう新しい方法が見つかった,という話は聞いたことがないし,どのくらいの一般論ができているのかも寡聞にして知りません。
2013-03-03 16:19:59@srb_2 本当は,こういう話は,集合論にどっぷりつかる前に大学の授業とかでやるといいと思うんですけど,知っている人が少ないのと今のところあんまり流行ってないのとで,残念ながら勉強しづらい雰囲気です。
2013-03-03 16:22:19@srb_2 集合論において,強制法やウルトラパワーが何でこんなにうまくいっているんだろう,他のモデルの作り方が何でなかなかでてこないんだろう,という問題を考える上では,とてもいいトピックだと思うんですけどね。
2013-03-03 16:24:00