計算論家トリイロさんと集合論家DIkeさんの対話

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi fine structure theory は，考えている構造（例えば Jα）の projectums と standard parameters がわかればその構造についてのほぼ全てのことがわかるように設計されています。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi 二つの fine structural な構造の間の射も，projectum や standard parameter を保つものになっていて，こういった「圏論的な」構造を理解することで L やその他の内部モデルを理解しようとするわけです。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi 先程の問いにもう少し素朴に答えると，fine structure では，L で GCH とか証明するときに使う condensation をもっと細かく見ている感じです。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi Kunen の本には，condensation は ZF-Power Set のモデルに対して書いてありますが，そういうのをぎりぎりに弱めたのが J-hierarchy で，condensation は任意の Jα に対して成り立ちます。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi そういう意味では，ゲーデルが L についてやったことを "boldface" とすると，ジェンセンが L についてやったことは "lightface" となっていると思います。

Takayuki Kihara @tri_iro

@DaiskeIkegami @tenapi あ、すいません、帰路についていたので返事が遅れました。ご丁寧に教えてくださってありがとうございます。なるほど、やはり根本的な発想は、boldfaceの話を一旦lightfaceに戻してboldfaceに持ち上げるという形なのですね。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi そうですね。エフェクティブな記述集合論にしても fine structure にしても，既存の研究対象や数学的現象をもう少し細かく調べてもっと詳しく理解しようよ，という方向で発展していった印象があります。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi どちらの場合も，より詳しい理解を得た後に全く新しいものを産みだして大成功しているのかなぁ，と思います。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi いろんなことが conceptual に整理されて，物事が進んでいっている感じがします。

紫陽花の葉に青蛙とゼルプスト殿下 @tenapi

エフェクティブな記述集合論の成功例といえば、ルーヴォーが切り口問題を解決したときも、まったくboldfaceなクラシカルな問題にlightfaceなアプローチをして成功したんだった。

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi あ，もうちょっとテクニカルに返信すると，例えば square principle についてだと，先程述べた fine structural な構造間の射を集めて束にしたものを club の coherent sequence にして，

Ikegami Daisuke @DaiskeIkegami

@tri_iro @tenapi 望みの boldface なオブジェクトを作っている感じです。そういう意味で，@tri_iro さんが指摘しているような boldface と lightface の間の話になってます。

H. Miyoshi (ALC Japan is rescheduled in 2025) @metaphusika

@DaiskeIkegami @tri_iro @tenapi 横からすみません。fine structureの「圏論的な」構造というのは例えばDevlinのConstructibilityに書いてあるような話のことでしょうか。その後の進展はフォローしていないので興味があります。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi 僕は Devlin の本をきちんと読んでいないのでお答えできるかわかりませんが，例えば，Jα があるとき，その first projectum ρ1，1st standard parameter p1 を考え，

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi ρ1 cup {p1} の元たちをパラメータとした Jα の Sigma1 theory A1 を考えると，Jα は (Jρ1, in, ρ1, A1) から自然に復元できます。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi こういった構造を Jα の first reduct と言うんですが，1st reduct を取る，という操作は iterate できて，

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi この操作を任意有限回（もうちょっと言うと final projectum に達するまで）繰り返して得られる構造たちと projectums やパラメータたちを「圏論的構造」と呼びました。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi Devlin の本だと，reductをiterate する代わりに直接 Sigma_n projectums や n 番目の standard paramerters を見ているかもしれませんが，本質的には同じものです。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi First reduct は一般の n-th reduct より扱いやすく，Skolem function も lightface で取れるので，

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi 現代の fine structure theory では，n-th reduct を見るより，first reduct の iterate を見ることが多いです。

H. Miyoshi (ALC Japan is rescheduled in 2025) @metaphusika

@DaiskeIkegami @tri_iro @tenapi ありがとうございます。こちらでも http://t.co/oxaWsprSrM を見つけたので池上さんのツイートと合わせてみると（私の誤解でなければ）iterateするほうが確かにより直接的ですね。腑に落ちました。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi Ralf と Martin の handbook article ですね。ええ，最近の fine structure の文献ではみんな first reduct を iterate してます。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi 先程述べた Skolem function の話では，Sigma1 だと lightface で Skolem function が取れるものの，Sigma2 で考えると lightface で取れない例があります。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi また，巨大基数を持つ fine structural な構造を考えると，先程述べた「圏論的」な構造を保つ射で Sigma2 truth を保存するのが不可能な例もあります。

Ikegami Daisuke @DaiskeIkegami

@metaphusika @tri_iro @tenapi というわけで，現代の fine structure theory には，Sigma_n を見る代わりに Sigma1 を iterate したものを見ざるをえない事情があります。