集合論家DIkeさんと証明論家GLogさんの対話

Ryota Akiyoshi（秋吉亮太） @georg_logic

僕が知っているのは順序解析周辺の証明論のドイツ人ばかりだけれど，たいてい正直で研究のレベルもとても高い．どうやら博士論文もかなりいい結果が出るまでやるらしく，この分野で博士号をとる年齢がどんどん遅くなっている気がする．

Ryota Akiyoshi（秋吉亮太） @georg_logic

分野のレベルを保つためにはとてもいいやり方だと思うけれど，もっと若いときに出版物がないと最近の傾向からすると厳しいのかもしれない．

Ikegami Daisuke @DaiskeIkegami

@georg_logic こんにちは，カリフォルニアで集合論をやっている池上と申します。数年前にミュンスターにいたとき，Pohlers さんのお弟子さんたちもそんな感じでしたね。僕みたいな素人から見ても大分良く見える結果を出した学生さんが，学位を取ったあとアカデミアを去るとか。

Ikegami Daisuke @DaiskeIkegami

@georg_logic アカデミアを去る理由を聞いたら，「僕はアカデミアに長くいすぎたよ」みたいな返事が返ってきたり。

Ikegami Daisuke @DaiskeIkegami

@georg_logic ドイツの場合，Ph.D. を持っていると就職しやすかったり，社会でもちょっと特別扱いされるので，日本と比べてアカデミアを出やすいんでしょうね。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami なるほど、確かにそういうケース割と聞きます。ハビリタチオンまでやって、Googleに就職、という例も聞きました。

Ryota Akiyoshi（秋吉亮太） @georg_logic

そういえば、証明論やっているドイツ人の友人も、そろそろ証明論から分野変えるとかいっていたような。研究所勤めは続けるらしいけど、data analysisとかいってた。

Ikegami Daisuke @DaiskeIkegami

@georg_logic ドイツで順序数解析をする研究者が減ってきているのは非常に残念なことです。僕は証明論にはとても疎いのですが，外から見た感じだと，順序数解析みたいなコアな分野が証明論の原動力になっている部分があると思うので。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami ドイツでの証明論は、かなりの程度収束に近づいていると思います。確かに、順序解析のために色々なテクニックが開発されたと思います。

Ikegami Daisuke @DaiskeIkegami

@georg_logic 集合論だと内部モデル理論がそんな感じで，多くの集合論のトピック・理論が，内部モデルプログラムの下で，発展・展開されてきました。

Ikegami Daisuke @DaiskeIkegami

@georg_logic 何か大きな目標・プログラムを持っている分野は，（それが途絶えない限り）強さがあるし，発展を続けていく，という印象があります。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami ですね。ただ、順序解析は、もはや複雑になり過ぎて、なにをもってなにを分析しているのか判断が難しい印象があります。あらい先生の最近の仕事はこの観点からも面白いです。ZFの（ある意味での）順序解析です。

Ikegami Daisuke @DaiskeIkegami

@georg_logic まぁ，そんな感じで，証明論における順序数解析，集合論における内部モデル理論の行く末には心配していますし，内部モデル理論の方は頑張っていきたいと思ってます。

Ryota Akiyoshi（秋吉亮太） @georg_logic

ジラールは、証明論は時間がかかる、といって順序解析周辺から分野をうつしたらしいが、ほんとかな。

Ikegami Daisuke @DaiskeIkegami

@georg_logic ええ，僕は全く知りませんが，新井先生の ZF の順序数解析の話には少し興味を持っています。テクニックとして，L の fine structure みたいなものを使うらしいので，集合論のほうから何か提供できるものがあればなぁ，と思ってます。

Ikegami Daisuke @DaiskeIkegami

@georg_logic ハビリタチオン取った後でも就職できるんですね。そういう話があるというのは，知りませんでした。

Ikegami Daisuke @DaiskeIkegami

@georg_logic 門外漢からすると，ZF の proof theoretic ordinal について何がわかれば目標達成と言えるのか，というのがちょっとわかりづらい感じです。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami あらい先生の仕事については、今までのリカーシブな証明論を持ち上げたので、どの部分ももちあげられるのか、というのが自然な問いだと思います。二階算術の部分体系の独立性命題を持ち上げたら、対応する集合論のそれになるのか、等。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami 証明論的順序数を理解するには、結局、その体系のカット消去を理解する必要があって、これらが切り離せないのが一つの問題なんでしょうね。なので、証明論的順序の計算から出てくる、独立性命題や、定義可能な関数の形で問題を立てることも多い気がします。

Ikegami Daisuke @DaiskeIkegami

@georg_logic きっと基本的なことだと思いますが，証明論的順序数の計算から出てくる独立性命題について，もし簡単な例がありましたら，一つ挙げていただけるとありがたいです。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami PAならばパリス、ハーリントン、Pi11-CAならばブフホルツのヒドラゲームでしょうか。

Ikegami Daisuke @DaiskeIkegami

@georg_logic 教えていただきありがとうございます。ブフホルツのヒドラゲームについては全く知りませんでした。僕の印象では，こういった独立性命題は，ある論理体系の証明論的順序数の計算の前に導入されていて，順序数解析が進んでからいろいろわかってくる，という印象なんですが，

Ikegami Daisuke @DaiskeIkegami

@georg_logic ZF に対してこういった独立性命題（あるいはその候補）で，ZF の証明論的順序数を調べることでその独立性やより詳しいことがわかってきそうなもので，現代集合論でその独立性がわかっていない（かもしれない）ものって，何かありますかね？

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami ちょっと即答は難しいですね、すいません。個人的には、ブフホルツのヒドラゲームを、何らかの意味で非再帰的にすればできるのでは、と勝手に思っていました。あらい先生に聞いてみたところ、考えたことなかった、とのご返答でした。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@DaiskeIkegami ただ、ZFの再帰的な意味での普通の順序解析は、まだ全く手がつけられていないので、そこから出てくる独立性命題はちょっと見当つかないです。あらい先生、Rathjenの成果はPi12-CAまでですので。