ファイル置き場 Sendai Logic Homepage 111202omoto

２階算術における強制法

小本健司

2011/12/02

論文の目次

◮ 準備

◮ _二階算術

◮ forcing の基本概念

◮ Tagged Tree Forcing

◮ _Π¹

1-SEP0̸→ Σ¹1-AC0 (Steel, Montalb´n)

◮ _∆¹

1-AC0̸→ Π¹1-SEP0(Montalb´n)

◮ _weak-Σ¹

1-AC0̸→ INDEC (Neeman)

◮ _{INDEC ̸→ ∆}¹

1-CA0 (Neeman)

◮ _∆¹

1-AC0̸→ ABW0 (Conidis)

◮ _そして...

◮ _Harringtonの定理など

今日のテーマ

◮ Tagged Tree Forcing^{の部分を解説する}.

◮ Steel.(1977)^はTagged Tree Forcing^で, ∆¹₁-CA0∧ ¬Σ¹₁-AC0

のモデルを構成した_.

◮ _∆¹_{1-CA0⇐ Π}¹_{1-SEP0⇐ Σ}¹_1-AC0

◮ Montalban(2008)^はSteel^{のモデルが}Π¹₁-SEP0^{のモデルでも}

あることを示し_{, ∆}¹_{1-CA0∧ ¬Π}¹_1-SEP0のモデルも構成した_.

◮ Tagged Tree Forcing^は Neeman(2008)Conidis(2010)^などで も_{, ∆}¹_{1-CA0∼ Σ}¹_1-AC0周辺の公理の分離に使われている_.

∆

-CA

̸→ Σ

-AC

定理

∆¹₁-CA0 ̸→ Σ¹₁-AC0

∆¹1-CA0≡∀n(φ(n) ↔ ¬ψ(n))

⇒ ∃X ∀n(n ∈ X ↔ φ(n)) Π¹1-SEP0≡¬∃n(¬φ(n) ∧ ¬ψ(n))

⇒ ∃X ∀n[(¬φ(n) → n ∈ X ) ∧ (n ∈ X → ψ(n))] Σ¹1-AC0≡(∀n)(∃X )φ(n, X ) ⇒ (∃Z )(∀n)φ(n, Z )

ただし_{, φ, ψ}は任意の_Σ

1

1^-formula.

Poset I

定義

p = ⟨T^p, f^p, h^p⟩ ∈ P ^{を以下で定義する}.

◮ _T^p_{⊆ ω}^<ω は 有限木

◮ _f^p は空でない有限関数で_{, dom f}^p_{⊆ ω, ran f}^p_{⊆ T}^p

◮ _h^p_{: T}^p_{→ ω1}^CK_{∪ {∞}} であり_,以下を満たす_.

◮ _{(∀s, t ∈ T}^p)[s ( t → h^p(s) > h^p(t)]

◮ _{(∀s ∈ T}^p)[(∃i)[s ⊆ f^p(i)] → h^p(s) = ∞]

定義

p ≤ q(for p, q ∈ P)^{を以下で定義する}.

◮ _T^q_{⊆ T}^p

◮ ^◮ _{dom f}^q_{⊆ dom f}^p

◮ (∀i ∈ dom f^q)[f^q(i) ⊆ f^p(i)]

◮ (∀i ∈ dom f^q)¬(∃s ∈ T^q)[f^q(i) ( s ⊆ f^p(i)]

◮ _h^q_{= h}^p _↾T^q

Poset II

定義

このとき, P-generic G ^に対し,

◮ _{T = T}^G _{:= ∪p∈GT}^p

◮ _α^G_{i = f}^G_{(i) := ∪}

p∈G ,i ∈dom f^pf p_(i)

◮ _{h = h}^G _{:= ∪p∈Gh}^p

と定義すると_{, T}^G は無限木_{, f}^G_(i)は_T^G の_pathであり_, h^G(s) =

{ |s|_T (if s ∈ WF (T^G))

∞ (if s /∈ WF (T^G))

すなわち_{, h}^G は_T^G のwellfounded part ^のrank function^になる. 以下, generic G を一つ固定して議論する_.

モデルの定義

定義

α < ω₁^{CK とする}.

この時_{, formula}の計算可能な列 _{⟨ψi | i ∈ ω⟩}であって_, 各_ψiが_Σ

0

βi^{-formula(βi < α)}であるようなものに対し_, φ = ∨_{i ∈ω}ψ_i ^の形のformula^をΣ⁰_α-formula^と呼ぶ. Σ⁰_α-formula^{の否定の形の}formula^をΠ⁰_α-formulra^と呼ぶ.

M_F := {X | (∃µ < ω^CK1 )[X ^はΣ⁰_µ({T^G} ∪ {α^G(i) | i ∈ F })^集合]} M∞:= ^∪

F ⊆finω

MF

以降で_{, M∞Π}¹_{1-SEP0∧ ¬Σ}¹_1-AC0 を示していく

¬Σ

-AC

定理

M∞2Σ¹₁-AC0

証明_.

◮ 各_MF は_T の_pathを有限本しか含まない_.

◮ _M∞=^∪

F ^{MF より, M∞はT のpathを無限本含む.}

◮ _{ψ(n, X ) ⇔def X0· · · Xn}は_Tの_pathは_{, Σ}

1

1^-formula.

◮ _M∞(∀n)(∃X )ψ(n, X ).

◮ しかし_{, ¬∃Z ∈ MF}(∀n)ψ(n, Z ).

◮ _M∞2(∃Z )(∀n)ψ(n, Z ). 証明終_.

Forcing Language & Notion I

定義

F ⊆fin ω^に対し, LF は以下からなる言語と定義する_.

◮ ∈, =, +×, ≤, 0, 1

◮ 数変数x, y , z, · · · , ^集合変数X , Y , Z , · · ·

◮ _{XF, YF, ZF}, · · · , X_F^ν, Y_F^ν, Z_F^ν, · · · , X^ν, Y^ν, Z^ν, · · ·

◮ _{T , ˙}˙ _αi (for i ∈ F )

◮ _Hν,F^˙ _{,Sν,F ,e}^˙

ただし_{, ν < ω}^CK_{1 , e ∈ ω}は任意にとる_.

◮ _{HF ,1:= T}^G _⊕^⊕

i ∈F^{αG(i), HF ,µ:=}

⊕

ν<µ,e∈ω^W H_{F ,ν} e

◮ _{Sµ,F ,e := We}^{HF ,µ}

S_{µ,F ,e} ^はΣ⁰_µ({T^G} ∪ {α^G(i) | i ∈ F }) ^{集合を表す},^変数のrank µ は_,値である集合が_Σ

0

µ^{であることを意味する.}

L∞:=^∪_{F ⊆}

finω^{LF と定める.}

Forcing Language & Notion II

定義

p ∈ P^とL∞formula ψ ^に対し, p ψ ^{を以下で定義する}.

◮ _{p ψ ⇔def ψ (ψ}が_L2 - quantifier free^の場合)

◮ _{p σ ∈ ˙T ⇔def}

(lh(σ) < 2 ∧ σ ∈ T^p) ∨ (1 ≤ h^p(σ⁻) ∧ σ⁻∈ T^p)

◮ _{p ⟨¯n, ¯m⟩ ∈ αi ⇔def i ∈ dom f}^p_{∧ f}^p_{(i)(n) = m}

◮ _{p n ∈ Sν,F ,e ⇔def} p (∃s)R(H_ν,F; e, s, n) (^ここでR^は universal TM^{を表現する}∆⁰₀-formula)

◮ _p ^∧

i ∈ω^{ψi ⇔def} (∀i ∈ ω)o ψ_i

◮ p ¬ψ ⇔ (∀q ≤ p)q 1 ψ

◮ p ⟨e, n, ν⟩ ∈ Hµ,F ⇔def ν < µ ∧ p n ∈ Sν,F ,e

◮ p ∀xψ(x) ⇔def (∀n ∈ ω)p ψ(n)

Forcing Language & Notion III

定義

◮ _{p ∀X}^µ F^ψ(X

µ

F^{) ⇔def} (∀ν < µ)(∀e ∈ ω)p ψ(Sν,F ,e)

◮ _{p ∀XFψ(XF) ⇔def (∀ν < ω}^CK₁ )(∀e ∈ ω)p ψ(S_{ν,F ,e})

◮ _{p ∀X}^µ_ψ(X^µ_{) ⇔def}

(∀ν < µ)(∀e ∈ ω)(∀F ⊆fin ω)p ψ(Sν,F ,e)

◮ _{p ∀X ψ(X}^µ F^{) ⇔def}

(∀ν < ω^CK1 )(∀e ∈ ω)(∀F ⊆fin ω)p ψ(Sν,F ,e)

変数の_{rank µ}は_,値である集合が_Σ

0

µ^{であることを意味する.}

補題

L2-formula ψ^に対し, M∞ψ ⇔ (∃p ∈ G )[p ψ]

Forcing Language & Notion IV

定義

1. ^変数がF-restricted ⇔_def G ⊆ F が変数の腰に付いている_. 2. formula^がF-restricted ⇔_def bounded variable^が全て

F-restricted

3. ^変数がranked ⇔_def ^{変数の肩に}rank(^順序数)^{が付いている}. 4. formula^がranked ⇔_def bounded variable^が全てranked また, ranked formula psi ^に対し,

rk(ψ) := ω1^CK· u(ψ) + ω²· o(ψ) + ω · r (ψ) + n(ψ) と定義する_. ただし_,

◮ o(ψ) := sup({ν | ν^はψ^のbounded variable^のrank} ∪ {ν + 1 | ψ^にS_{ν,F ,e}^またはH_ν,F^{の形の定数が出現する}})

◮ u(ψ) := (rank^{付き変数の個数})

◮ _{r (ψ) := (}の中のranked quantifier^個数)

◮ n(ψ) := (∧, ∨^の個数)

Retagging I

定義

p, p^∗ ∈ P, µ, F ⊆fin ω ^に対し,^同値関係Ret(µ, F , p, p^∗)(p^はp^∗の µ-F -retagging)^を

1. T^p= Tp^∗

2. (∀i ∈ F )[f^p(i) = fp^∗(i)]

3. (∀s ∈ T^p)[h^p(s) ≥ µ → h_p∗(s) ≥ µ] 4. (∀s ∈ T^p)[h^p(s) < µ → h^p(s) = h_p^∗(s)] で定義する_.

Retagging^はTagged Tree Forcing^{の肝である}.

Retagging II

補題

L_F-ranked-formula ψ ^とp, p^∗∈ P^に対し, Ret(ω · rk(ψ), F , p, p^∗) =⇒ (p ψ ⇔ p^∗ ψ)

補題

Ret(ωβ, F , p, p^∗) ∧ q ≤ p ∧ (γ + |T^q\ T^p| ≤ β)

=⇒ (∃q^∗ ≤ p^∗)Ret(ωγ, F , q, q^∗)

ただし_,|T^q_{\ T}^p_|は有限集合_T^q_{\ T}^pの濃度_.

Σ-over-L

I

定義

formula ψ^が, F-restricted formula ^を∧, ∀n, ∃X ^{で結合した形であ} るとき_{, ψ}は _Σ-over-LF であると言う_.

formula ψ^とµ < ω₁^{CK に対し},

ψ^µ:= (ψ^の∃X ^を∃X^{µで置き換えたもの}) 補題

ψ^をΣ-over-LF formula, µ < ω^CK1 ^とする.

このとき_{, ψ} に含まれる任意の定数記号_c に対しo(c) < µ ^が成り 立つならば_,

ψ^µ→ ψ が成り立つ_.

Σ-over-L

II

補題

1. p ψ ^かつ ψ ^がΣ-over-LF ^{であるとき},

(∃µ < ω1^CK)(∀ρ)[µ ≤ ρ < ω^CK1 → p ψ^ρ] が成り立つ_.

2. M_F Σ¹₁-AC0,^{したがって}M_F ^はhyperarithmetically closed. さらに_{, MF = HYP(T ⊕}

⊕

i ∈F^αGi ⁾

Σ-over-L

^と Retagging

補題

F ⊆fin ω, ψ ^をΣ-over-LF-sentence, µ < ω^CK₁ ^に対し,

Ret(ωrk(ψ) + ω², F , p, p^∗) ∧ dom f^p⊆ F =⇒ (p  ψ^µ⇒ p^∗ ψ^µ) 補題

F ⊆_fin ω, ψ ^をΣ-over-L_F-sentence, µ < ω^CK₁ ^に対し, Ret(ωrk(ψ) + ω²+ ω, F , p, p^∗) ∧ dom f^p ⊆ F

=⇒ (p  ¬ψ^µ⇒ p^∗ ¬ψ^µ)

下の補題は_Montalb´anが証明した補題で_{, Steel}の原論文に欠けて いたものである_. この補題のお陰で_Π

1

1-SEP0^{が証明できる}.

M

^{ Π}

^-SEP

^I

定理

M∞Π¹₁-SEP0

証明_.

M∞(∀n)[ψ(n) ∨ φ(n)] ^となるφ(n), ψ(n)^をΣ-over-LF formula に対し_{, M∞}(∀n)[(¬φ(n) → n ∈ D) ∧ (n ∈ D → ψ(n))]^となる D ∈ M∞^{を構成する}.

p ∈ G^{が存在して}, p (∀n)[ψ(n) ∨ φ(n)].

µ < ω₁^{CK を}, ψ, φに出現する任意の定数記号_cに対しµ > o(c)^と なるようにとる_.

ν < ω^CK₁ ^をran h^p ⊆ ν ∪ {∞} ∧ rk((∀n ∈ ω)ψ^µ(¯n) ∨ φ^µ(¯n)) < ν であるようにとる_.

M

^{ Π}

^-SEP

^II

q ∈ P_ω·ν+ω²_+2ω が存在し以下を満たすとき_{, d ∈ D}と定義する_.

◮ _{q ¬φ}^ν_(d)

◮ _T^q_{⊆ T}^G

◮ _h^qは_{(ων + ω}

2+ 2ω)-good

◮ (∀i ∈ F )[f^q(i) = α^G_i ∩ T^q]

ただし「_{g : T}^′ _{→ ω1}^CK _{∪ {∞}(T}^′_{⊆fin T}^G₎が_ν-good」を_, (h^G(s) < ν → g (s) = h^G(s)) ∧ (h^G(s) ≥ ν → g (s) ≥ ν) q ∈ Pν^を,

hq⊆ ν ∪ {∞} と定義する_.

q ¬φ^ν(d)^が(Steel^{の原論文では}q φ^ν(d)^だった. φ^ν(d)^では

∆¹1-CA0^{しか示せない}) このとき_{, D ≤H T ⊕}

⊕

i ∈F^αGi ^{より, D ∈ MF ⊆ M∞.}

M

^{ Π}

^-SEP

^III

¬φ(n) → n ∈ D^を示す_.

¬φ(n)^より¬φ^µ(n)^{が成り立つ}. q^∗ ∈ G ^をq^∗ ≤ p ∧ q^∗ ¬φ^µ(n) が成り立つようにとる_.

この時_{, q}^∗は_qの条件式を満たすが_{, q}^∗_{∈ Pων+ω}2_+2ωであるかは 分からない_. そこで _q を次のように定義すれば_{d ∈ D}の_witness となる_.

◮ _T^q_{= T}^q∗

◮ _f^q_{= f}^q∗

◮ _h^q_{(s) =}

{ h^q∗(s) (if h^q∗(s) < ων + ω²+ 2ω)

∞ (otherwise)

M

^{ Π}

^-SEP

^IV

¬ψ(n) → n /∈ D^を示す. ¬ψ(n) ∧ n ∈ D^{と仮定し背理法で示す.}

¬ψ(n)^よりr ∈ G ^が存在し, r ≤ p ∧ r ¬ψ^µ(n) n ∈ D ^より q ∈ G^が存在し, q ≤ p ∧ q ¬φ^µ(n)

p

↙ | ↘

¬φ^µ(n) ⊣ q | r ⊢ ¬ψ^µ(n)

↓ ↓ ↓

¬φ^µ(n) ⊣ q^∗ · · · s^∗ · · · r^∗ ⊢ ¬ψ^µ(n)

⊢ ¬φ^µ(n) ∧ ¬ψ^µ(n)

∆

-CA

̸→ Π

-SEP

定理(Montalb´an)

∆¹1-CA0 ̸→ Π¹1-SEP0

Π¹1-SEP0 ̸→ Σ¹1-AC0を微修正するだけで示せる_.

Poset I

forcing language^{はそのまま}, Poset^{を変更する}. 定義

p = ⟨T^p, f^p, h^p⟩ ∈ P ^{を以下で定義する}.

◮ _T^p_{⊆ ω}^<ω は 有限木

◮ _f^p は空でない有限関数で_{, dom f}^p_{⊆ ω, ran f}^p_{⊆ T}^p

◮ _h^p_{: T}^p_{→ ω1}^CK_{∪ {∞}} であり_,以下を満たす_.

◮ _{(∀s, t ∈ T}^p)[s ( t → h^p(s) > h^p(t)]

◮ _{(∀s ∈ T}^p)[(∃i)[s ⊆ f^p(i)] → h^p(s) = ∞]

※ (∀n)[(⟨2n⟩ ∈ T^p∨ ⟨2n + 1⟩ ∈ T^p) → (⟨2n⟩ ∈ T^p∧ ⟨2n + 1⟩ ∈ T^p)]

※ (∀n)[(⟨2n⟩ ∈ T^p∧ ⟨2n + 1⟩ ∈ T^p) → (h^p(⟨2n⟩) =

∞ ∨ h^p(⟨2n + 1⟩) = ∞)]

◮ (∀i ∈ dom f^p)[f^p(i) ̸= ⟨⟩]

Poset II

定義

p ≤ q(for p, q ∈ P)^{を以下で定義する}.

◮ _T^q_{⊆ T}^p

◮ ^◮ _{dom f}^q_{⊆ dom f}^p

◮ (∀i ∈ dom f^q)[f^q(i) ⊆ f^p(i)]

◮ (∀i ∈ dom f^q)¬(∃s ∈ T^q)[f^q(i) ( s ⊆ f^p(i)]

◮ _h^q_{= h}^p _↾T^q

※ (∀i ∈ dom f^p\ dom f^q)(∀s ⊆ f^p(i))[|s| ≥ 2 → s /∈ T^q]

¬Π

-SEP

I

定理

M∞2Π¹1-SEP0

証明_.

ψ_j(n) ⇔_def ”T^Gは2n + j^で始まるpath^{を持たない}”

⇔ h^G(⟨2n + j⟩) ̸= ∞ と定義すると_{, ψj}は_Π

1

1^{で, M}∞¬(∃n)[ψ0(n) ∧ ψ1(n)]. S ∈ M∞^{が存在して},

M∞(∀n)[(ψ0(n) → n ∈ S) ∧ (ψ1(n) → n /∈ S)] を満たすと仮定して矛盾を導く_.

¬Π

-SEP

II

F ^をS ∈ M_F ^{となるように取る}.^この時, p ∈ G ^{が存在して}, p (∀n)[(ψ0(n) → n ∈ S) ∧ (ψ1(n) → n /∈ S)]^かつF ⊆ dom f^p m^をh^G(⟨2m⟩) = h^G(⟨2m + 1⟩) = ∞ ∧ ⟨2m⟩ /∈ T^{p となるように} とる_. ここで _{m ∈ S} と仮定しても一般性は失われない_{(m /∈ S}な ら_{, S}^cを_Sに置き換えればよい_{). q ∈ G} を

q ≤ p ∧ (q ¯m ∈ S) ∧ ⟨2m⟩ ∈ T^q∧ ⟨2m + 1⟩ ∈ T^{q となるように} とる_.

φ ⇔_def ((∀n)[(ψ0(n) → n ∈ S) ∧ (ψ1(n) → n ∈ S)] ∧ ¯m ∈ S) と定義する_.

q^∗≤ p ^をRet(ω · rk(φ), F , q, q^∗) ∧ h^q∗(⟨2m + 1⟩) ̸= ∞ ^となるよ うに定義する_. 具体的には以下のようにする_.

1. T^q∗:= T^q 2. f^q∗ := f^q↾F 3. h^q∗(s) :=

{ ωrk(φ) (if h^q(s) = ∞ ∧ s(0) = 2m + 1) h^q(s) (otherwise)

¬Π

-SEP

III

すると_{, q}^∗ _φより_{, q}^∗ _{¬ψ1( ¯m).} 一方_{, h}^q

∗(⟨2m + 1⟩) ̸= ∞ ^より, q^∗ ψ1( ¯m)^なので,^矛盾. したがって_{, S} は存在せず_{, M∞¬Π}

1

1^{-SEP0である.}

証明終_.

∆

-CA

定義

gRet≤(µ, p, p^∗)^{を以下で定義する}.

◮ _{Ret≤(µ, dom f}^p_{, p, p}^∗₎

◮ (∀m)[⟨m⟩ ∈ T^p∧ h^p(⟨m⟩) = ∞ → h^p∗(⟨m⟩) = ∞] Retと同様の補題が成り立つので_{, M∞∆}

1

1-CA0^を示せる. ^ただ し_{, gRet≤(µ, p, p}^∗) ⇒ (p ¬ψ ⇒ p^∗ ¬ψ^µ) ^{の形の補題は示せな} いので_{, M∞Π}

1

1-SEP0^{は導けない}. 定理

M∞∆¹1-CA0

ご清聴ありがとうございました

ご清聴ありがとうございました

参考文献

◮ Antonio Montalb´an ”On the Π¹1-separation principle”(2008)

◮ John. R. Steel ”FORCING WITH TAGGED TREE”(1977)

◮ Jeremy Avigad ”Formalizing forcing arguments in subsystems of second-order arithmetic”(1996)

◮ Stephen G. Simpson ”Subsystem of Second Order Arithmetic Second Edition”(2009)

◮ Gerald E. Sacks ”Higher Recursion Theory”(1990)