二階算術と集合論での決定性

nemototakako @nemototakako

HOD がなんなのかそもそも知らないのだけど、二階算術の \Delta1_2 周辺のわからなさと似てるとなると気になる。 Inner model theory seminar. http://t.co/xPliREeDUa

Ikegami Daisuke @DaiskeIkegami

@nemototakako Hereditarily Ordinal Definable sets の略で，x の transitive closure の任意の元が ordinal を parameter にして V で definable な x たちの集まりです。> HOD

Ikegami Daisuke @DaiskeIkegami

@nemototakako ZFC のモデルでの HOD のわからなさが二階算術の Delta^1_2 のわからなさに似ているかどうかはちょっとわかりませんが，

Ikegami Daisuke @DaiskeIkegami

@nemototakako Sigma^1_1-determinacy と Delta^1_2-determinacy の間の determinacy と inner model theory の対応は未だによく分かってません。

Ikegami Daisuke @DaiskeIkegami

@nemototakako Philip Welch さんが頑張っていることの一つのがその辺の話です。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 集合論における Sigma^1_1 と Delta^1_2 の間の pointclass Gamma の決定性のわからなさと，二階算術における Gamma-comprehension のわからなさには関係があるんじゃないかな，と思ってます。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 二階算術における Sigma^0_2 と Sigma^0_3 の間の pointclass Delta に必要な comprehension (Gamma-comprehension) と，集合論における Gamma-決定性に関連があるのでは，

Ikegami Daisuke @DaiskeIkegami

@nemototakako と妄想しているわけです。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 「Delta に必要な」→「Delta-determinacy に必要な」です。失礼しました。

nemototakako @nemototakako

@DaiskeIkegami ちょっと用語がよくわからないんだけど、pointclass Gamma って何ですか？

Ikegami Daisuke @DaiskeIkegami

@nemototakako Pointclass というのは実数の部分集合たちのあつまりで，例えば，Sigma^0_2 集合のあつまりは pointclass になり，通常 Sigma^0_2 と書きます。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 以前書いた Gamma や Delta というのは，pointclass の変数として使いました。

nemototakako @nemototakako

@DaiskeIkegami 丁寧な説明ありがとう。point class って何か（たとえば Wadge reducibility とか）について閉じてる必要は特にないの？

Ikegami Daisuke @DaiskeIkegami

@nemototakako 定義では必要ないんですけど，都合のいい一般論展開するときは，ベール空間からそれ自身への recursive function の逆像について閉じてるとか，有限の union, intersection について閉じてるとか仮定しますね。

Ikegami Daisuke @DaiskeIkegami

@nemototakako Wadge reducibility について閉じてることを仮定するかは option ですね。Lightface の (real を parameter にしない) pointclass とかを扱うときは仮定しません。(再帰的集合全体とか)

nemototakako @nemototakako

@DaiskeIkegami 私は相変わらず弱い決定性について調べてますが、 Borel 決定性があっても存在が言える決定性はせいぜい \Delta^1_2 位の複雑さで、一方証明論的な強さは \Delta^1_2-CA_0 を超えていくわけで（確か）この辺さっぱりわかりません。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 「存在が言える決定性」→ 「Comprehension Axiom が成り立つ formula たち」かな？

Ikegami Daisuke @DaiskeIkegami

@nemototakako そうなんだ。知りませんでした。Base theory は RCA0 とかですか？

nemototakako @nemototakako

@DaiskeIkegami その位強いとRCA_0 でも ACA_0 でも \Pi^1_1-CA_0 でもあまり変わらないかな。

nemototakako @nemototakako

@DaiskeIkegami Baire 空間のゲームだと \Sigma^0_2 決定性が \Pi^1_1-CA_0 と RCA_0 上同値なので、それ以上の強さなら base theory をそこまで弱くてもあんまり意味がないかな。

Ikegami Daisuke @DaiskeIkegami

@nemototakako おぉ，なるほど。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 集合論の場合も似たようなことはあって，determinacy がいくらあっても V に 巨大基数があることは証明できなくて，その代わり，巨大基数の無矛盾性を witness するもの (mouse) の存在と同値になることが多いです。

Ikegami Daisuke @DaiskeIkegami

@DaiskeIkegami @nemototakako たとえば，集合論だと，base theory を ZFC としたとき，Pi11 (lightface)-決定性と 0^# の存在が同値になりますが，

Ikegami Daisuke @DaiskeIkegami

@nemototakako 0^# の存在自体の無矛盾性の強さは到達不可能基数のそれより強いけど，0^# の存在から到達不可能基数の存在は導けません。

Ikegami Daisuke @DaiskeIkegami

@nemototakako 挙げてもらった二階算術におけるボレル決定性の例もこれと似た現象だと思います。