ファイル置き場 Sendai Logic Homepage

(1)

Hall’s theorem in reverse mathematics

榊原拓

2010/5/28

(2)

概要

本発表では組合せ論_, グラフ理論の定理である _Hall の定理 ₍グラフでは結婚定理 _[6]) の無限版の複雑さを考え_, それが RCA₀ 上で ACA₀ と同値であることを示す_.

• ^準備

• Hall’s theorem ^の証明

• ^{今後の展開}

(3)

概要

• ^準備

(4)

概要

• ^準備

(5)

概要

• ^準備

(6)

準備∼逆数学とは∼

• 数学の定理の複雑さを求めたい_.

• 「数学の定理は適切な公理と同値になる」という逆数学現象を用いてその複雑さを調べる_.

• 二階算術の枠組みの中で_, 特に内包公理に注目して調べる_.

内包公理：二階算術の論理式 _ϕ に対し

∃X∀x(x ∈ X ↔ ϕ(x))

(7)

∃X∀x(x ∈ X ↔ ϕ(x))

(8)

∃X∀x(x ∈ X ↔ ϕ(x))

(9)

∃X∀x(x ∈ X ↔ ϕ(x))

(10)

準備∼部分体系∼ Definition(RCA⁰)

1. ^基本公理 2. Σ⁰₁-^帰納法

3. ∆⁰₁-^内包公理 (^{再帰的内包公理}) Definition(ACA⁰)

1. ^基本公理 2. Σ⁰₁-^帰納法

3. Π¹₀-^内包公理 (^{算術的内包公理})

(11)

準備∼その他∼

Fact([1]Lemma III.1.3.)

以下の主張は RCA₀ 上で同値_. 1. ACA⁰,

2. Σ⁰₁-^内包公理,

3. ^{任意の一対一写像} h : N → N ^に対して, ^{その値域になる} X ⊆ N ^が存在_.

Fact(^{ケーニッヒの補題}.[1]Theorem III.7.2.)

次が ACA₀ 上で証明できる_. 有限分岐木 _T に対し以下が同値_. 1. T ^{は無限個の節をもつ},

2. T 上に無限の長さの道が存在する_.

(12)

以下の主張は RCA₀ 上で同値_. 1. ^ACA⁰,

2. Σ⁰₁-^内包公理,

(13)

以下の主張は RCA₀ 上で同値_. 1. ACA⁰,

2. Σ⁰₁-^内包公理,

(14)

Hall’s theorem^∼定義∼

■ _A_i：空でない自然数の有限集合_. Definition(transversal)

RCA₀ 上で以下を定める_. 有限集合の族 _{A = {A}_i _{| i ∈ I}} に対し_, 集合 _X が _A の transversal ^{であるとは}, ∀x ∈ X(x ∈ A_f_(x)) ^{を満たす全単射} f : X → I ^{が存在するときをいう}.

■ ここで_{, A} のインデックス _I は有限集合でも無限集合でもよい_. ここでは無限集合のときは可算無限集合と考えその場合は自然数 N で考える_.

■ インデックスが有限のとき_{, A} が transversal ^{をもつという主張は} Σ⁰₁ 論理式になる_.

A₀ = {0, 1, 2} ^A1 ^{= {1}} ^A2 ^{= {1, 3}}

X = {0, 1, 3}

(15)

A₀ = {0, 1, 2} ^A1 ^{= {1}} ^A2 ^{= {1, 3}}

X = {0, 1, 3}

(16)

A₀ = {0, 1, 2} ^A1 ^{= {1}} ^A2 ^{= {1, 3}}

X = {0, 1, 3}

(17)

A₀ = {0,1, 2} ^A1 ^{= {1}} ^A2 ^{= {1,}^3}

X = {0, 1, 3}

(18)

Hall’s theorem^{∼有限版の証明∼} Lemma(^有限版 Hall ^の定理)

次が RCA₀ 上で証明できる_{. I} を自然数の有限集合とする_. 有限集合族 A = {Ai | i ∈ I} ^{に対し以下が同値}.

1. A ^の transversal X ^{が存在する},

2. ^任意の J ⊆ I ^に対し |^∪_i∈J A_i| ≥ |J|^（これを Hall’s condition ^と呼ぶ）_.

(19)

Hall’s theorem^{∼有限版の証明∼}

2 ⇒ 1 ^を |I| = n ^に関する Σ⁰₁-^{帰納法で求める}.

Proof. |I| = 0 ^{のときは明らか}. |I| ≤ n − 1 まで主張が成り立つとする_.

Case1. ^任意の 1 ≤ k < n, 1 ≤ i₁ < · · · < ik ≤ n ^に対し |^∪_1≤l≤k ^Ai_l| ≥ k + 1 であるとする_{. |A}₁_{| ≥ 1} なので _x₁ _{∈ A}₁ をとり_,

B_i = A_i \ {x₁}(2 ≤ i ≤ n)

と定める_. このとき, 1 ≤ k < n, 2 ≤ i₁ < · · · < ik ≤ n ^に対し

|^∪_1≤l≤k B_i_l| = |^∪_1≤l≤k A_i_l \ {x₁}| ≥ k. よって帰納法の仮定から

{Bi | 2 ≤ i ≤ n} ^は transversal X ^を持つ. ^今, ^任意の i(2 ≤ i ≤ n) ^に対し x₁ _{6∈ B}_i ^なので, ^各 B_i ^{の定め方から} X _{∪ {x}₁_} ^は _A ^の transversal ^である.

(20)

Case2. ^ある 1 ≤ k < n, 1 ≤ i₁ < · · · < i_k ≤ n ^に対し |^∪_1≤l≤k A_i_l| = k ^であるとする_. 以下 _i₁ = 1, . . . , i_k = k ^とする. ^仮定より {A_i | 1 ≤ i ≤ k} ^は

transversal ^{をもつので}, ^{互いに異なる} x₁, . . . , x_k ^で x₁ ∈ A₁, . . . , x_k ∈ A_k ^となる集合 _X _{= {x}₁, . . . , x_k} ^が存在. ^このとき, | ^∪_1≤i≤k A_i| = k ^から

|^∪_1≤i≤k A_i| = |X| = k. ^ここで,

B_i = A_i \ ^∪

1≤j≤k

A_j (k + 1 ≤ i ≤ n)

と定める_. このとき_{, ∀i(B}_i _{6= ∅).}

(21)

任意に 1 ≤ r ≤ n − k, k + 1 ≤ i₁ < · · · < ir ≤ n ^をとる. ^このとき,

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

A_l_{| − k.} 1, . . . , k, i₁, . . . , i_r ^{は互いに異なるので}, Hall’s condition ^より

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

k+1≤i≤n ^Bⁱ ^は Hall’s condition を満たすので帰納法の仮定から

∪

k+1≤i≤n ^Bⁱ ^の transversal X^′ ^{が存在する}. ^さらに, B_i ^{の定め方から} X ∪ X^′ は _A の transversal ^である.

□

(22)

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

□

(23)

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

□

(24)

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

□

(25)

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

□

(26)

| ^∪

1≤j≤r

B_i_j| = | ^∪

1≤j≤r

B_i_j| + | ^∪

1≤l≤k

A_l| − k

≥ | ^∪

1≤j≤r

B_i_j ∪ ^∪

1≤l≤k

A_l| − k

= | ^∪

1≤j≤r

A_i_j _∪ ^∪

1≤l≤k

| ^∪

1≤j≤r

B_i_j| ≥ | ^∪

1≤j≤r

A_i_j ∪ ^∪

1≤l≤k

A_l| − k

≥ (r + k) − k = r. よって

∪

□

(27)

Hall’s theorem^{∼無限版の証明∼} Lemma(^無限版 Hall ^の定理)

次が ^ACA₀ 上で証明できる_. 有限集合族 _{A = {A}_i _{| i ∈ N}} に対し以下が同値_.

2. ^{任意の有限集合} J ⊂ N ^に対し |^∪_i∈J A_i| ≥ |J|.

Proof. 2 ⇒ 1 をケーニッヒの補題を用いて求める_. 以下のような木 _T を構成する_.

長さが _n の有限列 _τ が _T に属す ⇔ ∀m < n(τ (m) ∈ Am) ∧ {τ (0), . . . , τ (n − 1)} が _{A_m | 0 ≤ m ≤ n − 1} ^の transversal ^である.

(28)

Hall’s theorem^{∼無限版の証明∼} Lemma(^無限版 Hall ^の定理)

次が ^ACA₀ 上で証明できる_. 有限集合族 _{A = {A}_i _{| i ∈ N}} に対し以下が同値_.

2. ^{任意の有限集合} J ⊂ N ^に対し |^∪_i∈J A_i| ≥ |J|.

Proof. 2 ⇒ 1 をケーニッヒの補題を用いて求める_. 以下のような木 _T を構成する_.

長さが _n の有限列 _τ が _T に属す ⇔ ∀m < n(τ (m) ∈ Am) ∧ {τ (0), . . . , τ (n − 1)} が _{A_m | 0 ≤ m ≤ n − 1} ^の transversal ^である.

(29)

■ 各 _A_i の定め方から _T は有限分岐_.

■ 有限版 _Hall の定理から任意の _n _{∈ N} に対し _T に属す長さ _n の有限列が存在_.

■ ケーニッヒの補題から道がとれ_, そこから transversal ^がとれる.

(30)

(31)

(32)

(33)

(34)

Hall’s theorem^∼reverse^∼ Theorem

以下が ^RCA₀ 上同値である_. 1. ACA⁰,

2. ^無限版 Hall ^の定理.

Proof. 2 ⇒ 1 ^を示す. ^{一対一の写像} f : N → N ^をとる. ^各 i ∈ N ^に対し

A_i = {f (i)} ^{と定めると}, A = {A_i | i ∈ N} ^は Hall’s condition ^を満たす. Hall の定理より_{, A} の transversal X ^と全単射 g : X → N ^で ∀x ∈ X(x ∈ A_g(x)) ^を満たすものが存在する_. このとき, ∀i ∈ N∃x ∈ X(i = g(x) ∧ x = f (g(x))),

x ∈ X ⇔ x ∈ range(f ). ^よって X = range(f ).

□

(35)

Hall’s theorem Theorem

以下が ^RCA₀ 上同値である_. 1. ACA⁰,

2. ^無限版 Hall ^の定理.

Proof. 2 ⇒ 1 ^を示す. ^{一対一の写像} f : N → N ^をとる. ^各 i ∈ N ^に対し

A_i = {f (i)} ^{と定めると}, A = {A_i | i ∈ N} ^は Hall’s condition ^を満たす. Hall の定理より_{, A} の transversal X ^と全単射 g : X → N ^で ∀x ∈ X(x ∈ A_g(x)) ^を満たすものが存在する_. このとき, ∀i ∈ N∃x ∈ X(i = g(x) ∧ x = f (g(x))),

x ∈ X ⇔ x ∈ range(f ). ^よって X = range(f ).

□

(36)

Matching Theorem Definition(^グラフ)

RCA₀ 上で以下を定める_.

■ グラフ _G を _V _{⊆ N} と _E _{⊆ V × V} のペア _G _{= (V, E)} で定める_{. V} の要素を頂点_{, E} の要素を辺と呼ぶ_.

■ 特に_, 任意の辺の端点が異なるふたつの頂点の集合 _V₁_{, V}₂ に属するように頂点を分割できるとき_{, G} を二部グラフといい _G _{= (V}₁_{, V}₂_{; E)} で表記する_.

(37)

Matching Theorem Definition(^グラフ)

■ グラフ _G を _V _{⊆ N} と _E _{⊆ V × V} のペア _G _{= (V, E)} で定める_{. V} の要素を頂点_{, E} の要素を辺と呼ぶ_.

■ 特に_, 任意の辺の端点が異なるふたつの頂点の集合 _V₁_{, V}₂ に属するように頂点を分割できるとき_{, G} を二部グラフといい _G _{= (V}₁_{, V}₂_{; E)} で表記する_.

(38)

Matching Theorem Definition(^{マッチング})

■ グラフ _G に対しふたつの辺 (e, f ), (e^′, f^′) ∈ E ^{が独立しているとは}, e 6= e^′ ∧ e 6= f^′ ∧ f 6= e^′ ∧ f 6= f^′

を満たすときをいう_.

■ _G _{= (V, E)} に含まれる独立な辺の集合 _M をマッチングと呼ぶ_. Notation

A ⊆ V ^に対し,

■ _∂A := {v ∈ V | ∃a ∈ A((a, v) ∈ E)},

■ _A^˜ _{:= A ∪ ∂A.}

(39)

A ⊆ V ^に対し,

■ _∂A := {v ∈ V | ∃a ∈ A((a, v) ∈ E)},

■ _A^˜ _{:= A ∪ ∂A.}

(40)

A ⊆ V ^に対し,

■ _∂A := {v ∈ V | ∃a ∈ A((a, v) ∈ E)},

■ _A^˜ _{:= A ∪ ∂A.}

(41)

A ⊆ V ^に対し,

■ _∂A := {v ∈ V | ∃a ∈ A((a, v) ∈ E)},

■ _A^˜ _{:= A ∪ ∂A.}

(42)

Matching Theorem

図において赤い頂点が _A の要素だとすると青い点が _∂A の要素_.

(43)

Matching Theorem

Theorem(^結婚定理 Hirst. [6])

以下の主張は RCA₀ 上で ACA₀ と同値になる_.

可算無限で _A に属す各頂点の隣接点が有限個である二部グラフ

G = (A, B; E) ^に対し, G ^が A ^{のマッチングを持つ} ⇔ ^任意の A ^の有限部分集合 _S に対し |∂S| ≥ |S|.

■ _∂A _{↔ A ,}

■ マッチング ↔ transversal.

(44)

Matching Theorem

■ _∂A _{↔ A ,}

(45)

Matching Theorem

■ _∂A _{↔ A ,}

A₀ = {0,1, 2} ^A1 ^{= {1}} ^A2 ^{= {1,} ^3}

X = {0, 1, 3}

(46)

今後の展開

■ Linking(Menger ^の定理)

■ _Matroid

■ その他

(47)

今後の展開

■ Linking(Menger ^の定理)

■ _Matroid

■ その他

(48)

今後の展開 _(Linking) Definition(ω-link)

RCA₀ 上で以下を定める_. 有向グラフ _G _{= (V, E)} に対し_, 辺の集合 _P が ω-link ^{であるとは}, 以下の条件を満たすときをいう_.

• ∀(v, u), (v, u^′) ∈ P (u = u^′),

• ∀(v, u), (v^′, u) ∈ P (v = v^′).

X, Y ⊆ V ^が G ^上 ω-link ^{可能であるとは}, ^{以下の条件を満たす} ω-link P が存在するときをいう_.

• ∀x ∈ X∃v ∈ V \ X((x, v) ∈ P ),

• ∀v ∈ V \ X∀x ∈ X((v, x) 6∈ P ),

• ∀y ∈ Y ∃v ∈ V \ Y ((v, y) ∈ P ),

• ∀v ∈ V \ Y ∀y ∈ Y ((y, v) 6∈ P ).

• ∀v ∈ V \ X ∪ Y ∃w ∈ V \ X ∪ Y ((v, w) ∈ P ).

(49)

• ∀(v, u), (v, u^′) ∈ P (u = u^′),

• ∀(v, u), (v^′, u) ∈ P (v = v^′).

• ∀x ∈ X∃v ∈ V \ X((x, v) ∈ P ),

• ∀v ∈ V \ X∀x ∈ X((v, x) 6∈ P ),

• ∀y ∈ Y ∃v ∈ V \ Y ((v, y) ∈ P ),

• ∀v ∈ V \ Y ∀y ∈ Y ((y, v) 6∈ P ).

• ∀v ∈ V \ X ∪ Y ∃w ∈ V \ X ∪ Y ((v, w) ∈ P ).

(50)

• ∀(v, u), (v, u^′) ∈ P (u = u^′),

• ∀(v, u), (v^′, u) ∈ P (v = v^′).

• ∀x ∈ X∃v ∈ V \ X((x, v) ∈ P ),

• ∀v ∈ V \ X∀x ∈ X((v, x) 6∈ P ),

• ∀y ∈ Y ∃v ∈ V \ Y ((v, y) ∈ P ),

• ∀v ∈ V \ Y ∀y ∈ Y ((y, v) 6∈ P ),

• ∀v ∈ V \ X ∪ Y ∃w ∈ V \ X ∪ Y ((v, w) ∈ P ).

(51)

• ∀(v, u), (v, u^′) ∈ P (u = u^′),

• ∀(v, u), (v^′, u) ∈ P (v = v^′).

• ∀x ∈ X∃v ∈ V \ X((x, v) ∈ P ),

• ∀v ∈ V \ X∀x ∈ X((v, x) 6∈ P ),

• ∀y ∈ Y ∃v ∈ V \ Y ((v, y) ∈ P ),

• ∀v ∈ V \ Y ∀y ∈ Y ((y, v) 6∈ P ),

• ∀v ∈ V \ X ∪ Y ∃w ∈ V \ X ∪ Y ((v, w) ∈ P ).

(52)

今後の展開 _(Linking)

Definition(bipartite dual)

RCA₀ 上で以下を定める_. 有向グラフ _G _{= (V, E)} に対し_, その二部双対 G^′ = (V, V ^′; E^′) を以下の条件を満たすようにして定める_.

• V ^は ^G ^{と同じ頂点}^{. V} ^′ ^{:= {v}^′ ^{| v ∈ V },}

• E^′ ^{:= {(v, u}^′^{) | v ∈ ˜}^{u}}. Question([4].Theorem 4.3)

以下の主張が ^RCA₀ 上どの公理体系と同値になるか？

G = (V, E) をループを含まない可算無限有向グラフ_{, G} に対する二部双対を _G^′ _{= (V, V} ^′_{; E}^′₎ とする_{. X, Y ⊆ V} が与えられたとき以下は同値_.

1. X, Y ^が G ^上 ω-link ^可能.

1. (V \ X), (V \ Y )^′ ^が G^′ ^上 link.

(53)

• V ^は ^G ^{と同じ頂点}^{. V} ^′ ^{:= {v}^′ ^{| v ∈ V },}

• E^′ ^{:= {(v, u}^′^{) | v ∈ ˜}^{u}}. Question([4].Theorem 4.3)

以下の主張が ^RCA₀ 上どの公理体系と同値になるか？

G = (V, E) をループを含まない可算無限有向グラフ_{, G} に対する二部双対を _G^′ _{= (V, V} ^′_{; E}^′₎ とする_{. X, Y ⊆ V} が与えられたとき以下は同値_.

• X, Y ^が ^G ^上 ^ω-link ^可能^.

• (V \ X), (V \ Y )^′ ^が ^G^′ ^上 ^link.

(54)

• V ^は ^G ^{と同じ頂点}^{. V} ^′ ^{:= {v}^′ ^{| v ∈ V },}

• E^′ ^{:= {(v, u}^′^{) | v ∈ ˜}^{u}}. Theorem

以下の主張は ^RCA₀ 上で ^ACA₀ と同値になる_.

G = (V, E) をループを含まない可算無限有向グラフ_{, G} に対する二部双対を _G^′ _{= (V, V} ^′_{; E}^′₎ とする_{. X, Y ⊆ V} が与えられたとき_, 以下は同値_.

• X, Y ^に対し ^X ^は ^G ^上で ^Y ^の中に ^ω-link ^可能^.

• (V \ X) ^と ^{(V \ Y )}^′ ^を含む ^V ^′ ^{の部分集合が} ^G^′ ^上 ^link.

(55)

今後の展開 (Menger’s theorem)

有限版 Menger’s theorem(Menger 1927)

有限グラフ _G _{= (V, E)} と _{A, B} _{⊆ V} に対して_{, A, B} を分離させる最小の頂点の集合の基数は_, 互いに交わらない最大の _A-B 道の集合の基数と一致する_.

無限版 Menger’s theorem([5])

可算無限グラフ _G _{= (V, E)} と _{A, B} _{⊆ V} に対して_, 互いに交わらない A-B ^{道の最大の集合} P ^と A, B を分離させる頂点の集合 _S が存在し_{, S} は _P に属する各道から頂点を一つずつとった集合である_.

現在ある結果としては, Paul Shafer ^が MIT Logic

Seminar(Cambridge, MA 4.2.2008.) ^で Π¹₁-CA₀ ^{で証明できることを示} しているのみ_.

(56)

今後の展開 (Menger’s theorem)

有限版 Menger’s theorem(Menger 1927)

有限グラフ _G _{= (V, E)} と _{A, B} _{⊆ V} に対して_{, A, B} を分離させる最小の頂点の集合の基数は_, 互いに交わらない最大の _A-B 道の集合の基数と一致する_.

無限版 Menger’s theorem([5])

可算無限グラフ _G _{= (V, E)} と _{A, B} _{⊆ V} に対して_, 互いに交わらない A-B ^{道の最大の集合} P ^と A, B を分離させる頂点の集合 _S が存在し_{, S} は _P に属する各道から頂点を一つずつとった集合である_.

現在ある結果としては, Paul Shafer ^が MIT Logic

Seminar(Cambridge, MA 4.2.2008.) ^で Π¹₁-CA₀ ^{で証明できることを示} している_.

(57)

References

[1] Stephen. G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999.

[2] Mirsky. L, Transversal Theory, Academic Press(London)1971. [3] Marshall Hall, Jr, Combinatorial theory Second Edition, Wiley

,NewYork, 1986.

[4] Colin J. H. McDIARMID, Extensions of Menger’s theorem, Quart. J. Math. Oxford(3), 26(1975), 141-157.

[5] R. Aharoni, Menger’s theorem for countable graphs, J. Combin. Th., Ser. B, 43(1987), 303-313.

[6] Jery L. Hirst, Marriage theorems and reverse mathemarics, Cont. Math. 16 , pp.181-196, 1998.