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

(1)

Ordering ^の逆数学

小本健司

2011^年9^月2^日

(2)

Ordering の逆数学

1 ^順序とExtendibility^の定義 extendibility

2 Extendibility^{の逆数学的強さ} Ext(ω^∗)

Ext(Z) Ext(Q) 3 JUL

JUL FRA WQO(ST) FINDEC JUL(min-dec) 相関図 4 Problem

5 ^参考文献

(3)

順序とExtendibility の定義

Definition

h|P| , ≤Pi ^はpartial order(^半順序) x ≤P ^x

x ≤P ^y∧ y ≤P ^z → x ≤P ^z

x ≤P ^y∧ y ≤P ^x → x = y

Definition

Partial order L = h|L| , ≤_Li ^はlinear order(^線形順序) x _≤_Ly_{∨ y ≤}_Lx

Definition

Linear order W = h|W | , ≤Wi ^はwell order(^整列順序) 無限降下列を持たない

(4)

Ordering の逆数学順序とExtendibility の定義

extendibility

Definition

Linear order L = h|L| , ≤Li^はpartial order P = h|P| , ≤Pi^のlinear extension

|L| = |P|

p <_P q → p <L^q (i.e. <L⊇<P)

Theorem

無限降下列を含まないpartial order^はwell order^{であるような} linear extension^を持つ

(5)

順序とExtendibility の定義 extendibility

Definition

P ¹ Q ⇔def ^埋め込み^f ^{: P ˜}→Q ^{が存在する} P ∼ Q(P, Q^はequimorphic) ⇔_defP ¹ Q ∧ P º Q

Definition

Partial order P ^はscatterd ⇔_def_{Q P}

Theorem

Scatterd^なpartial order^はscatterd^なlinear extension^を持つ

(6)

Ordering の逆数学順序とExtendibility の定義

extendibility

Definition

Linear order ξ ^はextendible, Ext(ξ)

⇔def ^任意のpartial order P^について, ξ P ⇒ P^のlinear extension L^{が存在して}, ξ L

Example

ω, ω^∗,Z, ω^∗+ ω,Q^はextendible

2, 3, 4, · · · , ω + ω^∗ ^はextendible^ではない

(7)

Extendibility の逆数学的強さ

Ext(Z) Ext(Q) 3 JUL

5 ^参考文献

(8)

Extendibility の逆数学的強さ Ext(ω^∗)

Theorem

1 ACA₀ ⊢ Ext(ω^∗)

2 WKL₀ 0 Ext(ω^∗)

3 RCA₀+ Ext(ω^∗) ⊢ WKL₀

”P^はwpo → P ^はwell order^なlinear extension^を持つ” ^なら RCA0+ RT²₂^{で証明できる}.

(9)

WKL0 0 Ext(ω^∗)^の証明証明_.

X₀ <T ^X1 <T ^X2 <T · · · ^をuniformly low, uniformly ∆⁰₂ ^とする. S = {Y | ∃iY <_T Xi}^とすると, (ω, S) |= WKL₀+ ¬∃0^′

computable^なPartial order P ^{を次のように作る} P = ⊕_{i ,e}P_{i ,e}

各_P_{i ,e}はPartial Order^{で、互いに素} P_{i ,e}の無限降下列は、もし存在すれば₀

′

を計算できる L_{i ,e} = {e}^X_i ^{がもし存在し}, Li ,e⌈|Pi ,e|^がP_{i ,e}^のLinear Extension^{であるならば}, Li ,e ^{は無限降下列を持つ}

(^ここで、P_{i ,e} ^{の図を黒板に書きます}.)

{Xi}i^はuniformly ∆⁰₂^なので, uniformly^にrecursive^{に近似でき}

る_. 証明終

.

(10)

Problem

RCA₀+ Ext(ω) ⊢ ACA₀ ?

(11)

Extendibility の逆数学的強さ Ext(Z)

Theorem

RCA₀ ⊢ ATR0 ↔ Ext(Z)

(12)

Extendibility の逆数学的強さ Ext(Q)

Definition

RCA∗ = RCA₀+ Σ¹₁-IND ATR∗= ATR₀+ Σ¹₁-IND

Theorem

1 ATR∗ _{⊢ Ext(Q)} 2 WKL₀ 0 Ext(Q)

3 RCA₀+ Ext(Q) ⊢ WKL0 4 Σ¹₁-AC₀+ Ext(Q) ⊢ ATR0

Problem

RCA₀+ Ext(Q) ⊢ ATR0 ^?

(13)

JUL

Ext(Z) Ext(Q) 3 JUL

5 ^参考文献

(14)

Ordering の逆数学 JUL

JUL

Definition

L ^はleft indecomposable(L^は ←)

⇔def^L^{の任意の空でない}initial segment A^に対しL¹ A L ^はright indecomposable(L^は →)

⇔def^L^{の任意の空でない}final segment B^に対しL¹ B L ^はh→, ←i

⇔def→^なL₀^と, ←^なL₁^が存在し, L = L₀+ L₁

Example ω^は→

Q^は←^かつ→

Z^は←^でも→^でもない ω+ ω^∗^は h→, ←i

(15)

JUL JUL

Definition

L= A + B + C^のとき, B^はL^のessential segment

⇔def^L¹ A + B^′+ C → B ¹ B^′

Theorem (JUL, Jullian^の定理) scatterd linear order L^はextendible

⇔def^L ^の^全てのessential segment^は 2^でも h→, ←i^でもない JUL^{の逆数学的強さは？}

⇒ Big 5^{ではないらしい？} 同値な命題がいくつかある_.

(16)

FRA

Definition

FRA ⇔_deflinear order^{全体のクラスは}, ¹^についてwell quasi order i.e. ∀{Ln}n∃i < ∃j(Li º Lj)

Theorem

RCA∗ ⊢ FRA ↔ JUL

(17)

JUL WQO(ST)

Definition

{+, −}-labeled wellfounded tree^をsigned tree^と呼ぶ

Definition (WQO(ST))

Signed tree^{全体のクラスは}, ¹^についてwell quasi order i.e. ∀{Tn}n∈N∃i < ∃j(Ti ¹ Tj)

(18)

WQO(ST)

l^を∀i∃^∞n[l(n) = i]^{となる関数とする} Definition

lin(T ) =







1 (T = ∅)

∑

n∈ω^lin(Tl(n)⁾ (s(hi) = +)

∑

n∈ω^∗^lin(T^l(n)) (s(hi) = −)

Example

lin





+

ւ ց

+ −



∼ω+ ω^∗+ ω + ω^∗+ · · ·

(19)

JUL FINDEC

Definition

∃T (L = lin(T ))^{であるとき}, L^はh-indecomposable^であると言う

s_T(hi) = +^{であるとき}L^はright h-indecomposable ^と言う s_T(hi) = −^{であるとき}L^はleft h-indecomposable ^と言う

right(left) h-indecomposable ⇒ scatterd right(left) indecomposable

(20)

FINDEC

Definition

h-indecomposable^のタプルhF0^,· · · Fni ^はlinear order L^のfinite decomposition

⇔def^L∼^∑ⁿ_i₌₀F_n

finite decompositionのうち長さが最小のものを_minimal decomposition^という

Definition (FINDEC)

scatterd linear order^はfinite decomposition^を持つ

(21)

JUL JUL(min-dec)

Definition (JUL(min-dec))

scatted linear ordering L^がminimal decomposition hF₀,· · · , Fni^をもつとき

L^はextendible ⇔ ¬∃i < n[Fi = F_i+1 = 1 ∨ (Fi^is → ∧Fi+1^is ←)] minimal decompositionが存在するとは限らないので_,

JUL(min-dec)^はJUL^より弱い

(22)

JUL(min-dec)

Theorem

1 RCA₀ ⊢ FRA ↔ WQO(ST) ↔ FINDEC

2 RCA∗ ⊢ FRA ↔ JUL

3 RCA∗ ⊢ ATR∗ ↔ JUL(min-dec)

4 RCA₀+ FRA ⊢ ATR₀

5 RCA₀+ FRA0 Π¹₁-CA₀

6 Π¹₂-CA₀ ⊢ FRA, JUL

Theorem

ATR∗ ⊢ h-indecomposable^は extendible ATR∗ ⊢ Ext(Q)

(23)

JUL 相関図

相関図

(24)

相関図

Ext(Z) Ext(Q) 3 JUL

5 ^参考文献

(25)

Problem

RCA₀+ Ext(ω^∗) |= ACA₀?

ACA0^{より弱い公理系と、}Ext(ω^∗)^との関係 FRA ⇔ ATR₀

RCA₀ ⊢ Ext(Q) ↔ ATR0^?

RCA₀ ⊢ JUL(min-dec) ↔ ATR0^?

FRA, FINDEC, WQO(ST)^の, JUL(min-dec)^{との対応物は} 何か？

Orderingの他の定理に関する逆数学

(26)

Ordering の逆数学参考文献

References I

Rondey G Downey, Denis R Hirschfeldt, Steffen Lempp, D Reed Solomon. Computablity-theoric and Proof theoretic Aspects of Partial and Linear Orderings. 2003.

Antonio Montalb´an. Equivalence betweem Fra¨ıs´e’s conjecture and Jullien’s theorem. 2006.

Stephen G.Simpson. Subsystem of Second Order Arithmetic Second Edition. 2009