ファイル置き場 Sendai Logic Homepage speaker4

Recursive Marriage Theorems and Reverse

Mathematics

Makoto Fujiwara¹

Tohoku University

2012.2.21

1Joint work with Kojiro Higuchi and Takayuki Kihara

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 1 / 32

Contents

1 What is Reverse Mathematics?

2 Previous Study on the Strength of Marriage Theorems.

3 Marriage Theorems with a lot of acquaintances.

4 Marriage Theorems with a few acquaintances.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 2 / 32

What is Reverse Mathematics?

The aim of reverse mathematics is classifying the mathematical theorems by the difficulty.

We look for the set existence axiom which is exactly needed to prove each theorem. Actually, we check which set

existence axiom is necessary and sufficient to the theorem over base theory RCA₀.

Here RCA₀ consists of the following axioms.

1 Basic axioms of arithmetic.

2 _Σ⁰

1induction axiom.

3 _∆⁰

1(recursive) set existence axiom.

In reverse mathematics, we prove not only a theorem from axioms but also an axiom from the theorem. Then this research program is called “reverse mathematics”.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 3 / 32

What is Reverse Mathematics?

The aim of reverse mathematics is classifying the mathematical theorems by the difficulty.

We look for the set existence axiom which is exactly needed to prove each theorem. Actually, we check which set

existence axiom is necessary and sufficient to the theorem over base theory RCA₀.

Here RCA₀ consists of the following axioms.

1 Basic axioms of arithmetic.

2 _Σ⁰

1induction axiom.

3 _∆⁰

1(recursive) set existence axiom.

In reverse mathematics, we prove not only a theorem from axioms but also an axiom from the theorem. Then this research program is called “reverse mathematics”.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 3 / 32

What is Reverse Mathematics?

The aim of reverse mathematics is classifying the mathematical theorems by the difficulty.

We look for the set existence axiom which is exactly needed to prove each theorem. Actually, we check which set

existence axiom is necessary and sufficient to the theorem over base theory RCA₀.

Here RCA₀ consists of the following axioms.

1 Basic axioms of arithmetic.

2 _Σ⁰

1induction axiom.

3 _∆⁰

1(recursive) set existence axiom.

In reverse mathematics, we prove not only a theorem from axioms but also an axiom from the theorem. Then this research program is called “reverse mathematics”.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 3 / 32

What is Reverse Mathematics?

The aim of reverse mathematics is classifying the mathematical theorems by the difficulty.

We look for the set existence axiom which is exactly needed to prove each theorem. Actually, we check which set

existence axiom is necessary and sufficient to the theorem over base theory RCA₀.

Here RCA₀ consists of the following axioms.

1 Basic axioms of arithmetic.

2 _Σ⁰

1induction axiom.

3 _∆⁰

1(recursive) set existence axiom.

In reverse mathematics, we prove not only a theorem from axioms but also an axiom from the theorem. Then this research program is called “reverse mathematics”.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 3 / 32

What is Reverse Mathematics?

Although there are so many mathematical theorems, most of ordinary mathematical theorems are provable in RCA₀ or equivalent to WKL, ACA, ATR, or_Π¹₁-CA over RCA₀. RCA₀₍₊some strong induction axiom) corresponds to recursive mathematics and the equivalence to WKL, ACA... reveals how far is the theorem from holding recursively.

RCA₀ < WKL₀ < ACA₀ <ATR₀ <_Π¹₁-CA₀

Here WKL0 is the theory consisting of RCA0+^{WKL and so} on.

In my talk, let graphs be countable unless otherwise stated.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 4 / 32

What is Reverse Mathematics?

Although there are so many mathematical theorems, most of ordinary mathematical theorems are provable in RCA₀ or equivalent to WKL, ACA, ATR, or_Π¹₁-CA over RCA₀. RCA₀₍₊some strong induction axiom) corresponds to recursive mathematics and the equivalence to WKL, ACA... reveals how far is the theorem from holding recursively.

RCA₀ < WKL₀ < ACA₀ <ATR₀ <_Π¹₁-CA₀

Here WKL0 is the theory consisting of RCA0+^{WKL and so} on.

In my talk, let graphs be countable unless otherwise stated.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 4 / 32

What is Reverse Mathematics?

Although there are so many mathematical theorems, most of ordinary mathematical theorems are provable in RCA₀ or equivalent to WKL, ACA, ATR, or_Π¹₁-CA over RCA₀. RCA₀₍₊some strong induction axiom) corresponds to recursive mathematics and the equivalence to WKL, ACA... reveals how far is the theorem from holding recursively.

RCA₀ < WKL₀ < ACA₀ <ATR₀ <_Π¹₁-CA₀

Here WKL0 is the theory consisting of RCA0+^{WKL and so} on.

In my talk, let graphs be countable unless otherwise stated.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 4 / 32

Reverse Mathematics for Graph Theory

Theorem in Graph Theory

Π¹₁^-CA0 For a sequence of graphs, there exists a function chosing the graphs which has a Hamilton path.

ATR₀ For a sequence of graphs having at most one Ham. path, there exists a function chosing the graphs which has a Ham. path. ACA₀ K ¨onig’s lemma.

Marriage theorem and symmetric marriage theorem.

Every graph can be decomposed into connected components. Ramsey theorem forksize and2coloring. (k ≥ 3)

WKL₀ Marriage theorem and symmetric marriage theorem for highly recursive graphs.

   _Everyk-colorable highly recursive graph is (2k − 2)-colorable. Everyk-colorable graph ism-colorable. (m ≥ k ≥ 2)

RCA₀ Theorems for finite graphs.

Everyk-colorable highly recursive graph is (2k − 1)-colorable.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 5 / 32

Contents

1 What is Reverse Mathematics?

2 Previous Study on the Strength of Marriage Theorems.

3 Marriage Theorems with a lot of acquaintances.

4 Marriage Theorems with a few acquaintances.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 6 / 32

B^′_HGM(Infinite Marriage Theorem) (M.Hall, 1948)

A bipartite graph(B, G; R)which satisfies condition H and B^′, has a solution.

Condition H : For allX⊂_finB,

|X| ≤ |N(X)| (= |{g | ∃b ∈ X ((b, g) ∈ R)}| ) ^holds. Condition B^′ : For allb ∈ B,|N(b)| < ∞holds.

A solution : A injection f ⊂ RfromBtoG

.

.

.

.

.

.

B G

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 7 / 32

B^′_HGM(Infinite Marriage Theorem) (M.Hall, 1948)

A bipartite graph(B, G; R)which satisfies condition H and B^′, has a solution.

Condition H : For allX⊂_finB,

|X| ≤ |N(X)| (= |{g | ∃b ∈ X ((b, g) ∈ R)}| ) ^holds. Condition B^′ : For allb ∈ B,|N(b)| < ∞holds.

A solution : A injection f ⊂ RfromBtoG

.

.

.

.

.

.

B G

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 7 / 32

B^′_HGM(Infinite Marriage Theorem) (M.Hall, 1948)

A bipartite graph(B, G; R)which satisfies condition H and B^′, has a solution.

Condition H : For allX⊂_finB,

|X| ≤ |N(X)| (= |{g | ∃b ∈ X ((b, g) ∈ R)}| ) ^holds. Condition B^′ : For allb ∈ B,|N(b)| < ∞holds.

A solution : A injection f ⊂ RfromBtoG

.

.

.

.

.

.

B G

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 7 / 32

B^′_HGM(Infinite Marriage Theorem) (M.Hall, 1948)

A bipartite graph(B, G; R)which satisfies condition H and B^′, has a solution.

Condition H : For allX⊂_finB,

|X| ≤ |N(X)| (= |{g | ∃b ∈ X ((b, g) ∈ R)}| ) ^holds. Condition B^′ : For allb ∈ B,|N(b)| < ∞holds.

A solution : A injection f ⊂ RfromBtoG

B G

.

.

.

Figure: B_HGM does not hold. (Condition B^′can not be dropped.)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 7 / 32

Theorem. (Manaster-Rosenstein, 1972)

There exists arecursivebipartite graph(B, G; R)which satisfies condition H and B^′, but has norecursivesolution.

(B^′_HGM does not hold recursively.)

Condition B^′′ : The function p : B → ^N is recursive.

∈ ∈

b 7→ |N(b)| Condition G^′ : For allg ∈ G,|N(g)| < ∞holds.

Condition G^′′ : The function p : G → ^N is recursive.

∈ ∈

g 7→ |N(g)|

Theorem. (Manaster-Rosenstein, 1972)

There exists a recursive bipartite graph(B, G; R)which satisfies condition H, B^′′ and G^′′, but has no recursive solution.

(B^′′_HG^′′M does not hold recursively.)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 8 / 32

Theorem. (Manaster-Rosenstein, 1972)

There exists arecursivebipartite graph(B, G; R)which satisfies condition H and B^′, but has norecursivesolution.

(B^′_HGM does not hold recursively.)

Condition B^′′ : The function p : B → ^N is recursive.

∈ ∈

b 7→ |N(b)| Condition G^′ : For allg ∈ G,|N(g)| < ∞holds.

Condition G^′′ : The function p : G → ^N is recursive.

∈ ∈

g 7→ |N(g)|

Theorem. (Manaster-Rosenstein, 1972)

There exists a recursive bipartite graph(B, G; R)which satisfies condition H, B^′′ and G^′′, but has no recursive solution.

(B^′′_HG^′′M does not hold recursively.)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 8 / 32

Theorem. (Manaster-Rosenstein, 1972)

There exists arecursivebipartite graph(B, G; R)which satisfies condition H and B^′, but has norecursivesolution.

(B^′_HGM does not hold recursively.)

Condition B^′′ : The function p : B → ^N is recursive.

∈ ∈

b 7→ |N(b)| Condition G^′ : For allg ∈ G,|N(g)| < ∞holds.

Condition G^′′ : The function p : G → ^N is recursive.

∈ ∈

g 7→ |N(g)| Theorem. (Manaster-Rosenstein, 1972)

There exists a recursive bipartite graph(B, G; R)which satisfies condition H, B^′′ and G^′′, but has no recursive solution.

(B^′′_HG^′′M does not hold recursively.)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 8 / 32

Theorem (Hirst, 1990)

1

_RCA

_{⊢ B}

H

^{GM ↔ ACA}

2

_RCA

_{⊢ B}

H

^{GM ↔ WKL}

B^′′_HGM : A bipartite graph (B, G; R) which satisfies condition H and B^′′, has a solution.

Note that condition B^′′ is written as follows within RCA₀.

∃p : B → Nsuch that∀b, g((b, g) ∈ R → g ≤ p(b))

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 9 / 32

Theorem (Hirst, 1990)

1

_RCA

_{⊢ B}

H

^{GM ↔ ACA}

2

_RCA

_{⊢ B}

H

^{GM ↔ WKL}

B^′′_HGM : A bipartite graph (B, G; R) which satisfies condition H and B^′′, has a solution.

Note that condition B^′′ is written as follows within RCA₀.

∃p : B → Nsuch that∀b, g((b, g) ∈ R → g ≤ p(b))

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 9 / 32

B^′_HG^′_HM_s(Symmetric Marriage Theorem)

A bipartite graph(B, G; R)which satisfies condition H forBandG, B^′and G^′, has a symmetric solution (bijection f ⊂ RfromBtoG). Theorem (Hirst, 1990)

1

_RCA

_{⊢ B}

H

^G

′

H

^M

^{↔ ACA}

2

_RCA

_{⊢ B}

H

^G

′′

H

^M

^{↔ WKL}

B^′′_HG^′′_HM : A bipartite graph(B, G; R)which satisfies condition H for BandG, B^′′and G^′′, has a symmetric solution.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 10 / 32

B^′_HG^′_HM_s(Symmetric Marriage Theorem)

A bipartite graph(B, G; R)which satisfies condition H forBandG, B^′and G^′, has a symmetric solution (bijection f ⊂ RfromBtoG). Theorem (Hirst, 1990)

1

_RCA

_{⊢ B}

H

^G

′

H

^M

^{↔ ACA}

2

_RCA

_{⊢ B}

H

^G

′′

H

^M

^{↔ WKL}

B^′′_HG^′′_HM : A bipartite graph(B, G; R)which satisfies condition H for BandG, B^′′and G^′′, has a symmetric solution.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 10 / 32

Contents

1 What is Reverse Mathematics?

2 Previous Study on the Strength of Marriage Theorems.

3 Marriage Theorems with a lot of acquaintances.

4 Marriage Theorems with a few acquaintances.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 11 / 32

Theorem. (Manaster-Rosenstein, 1972 (Review)) B^′′_HG^′′M does not hold recursively.

Condition H^′ : Condition H and

∀n∃m∀X⊂_finB (|X| ≥ m → |N(X)| − |X| ≥ n) holds. Condition H^′′ : Condition H and

there exists a recursive functionh : N → Ns.t.

∀n∀X⊂_finB (|X| ≥ h(n) → |N(X)| − |X| ≥ n) holds. Theorem. (Kierstead, 1983)

B^′′_H′′G^′′M holds recursively. Theorem. (Kierstead, 1983) B^′′_H′G^′′M does not hold recursively.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 12 / 32

Theorem. (Manaster-Rosenstein, 1972 (Review)) B^′′_HG^′′M does not hold recursively.

Condition H^′ : Condition H and

∀n∃m∀X⊂_finB (|X| ≥ m → |N(X)| − |X| ≥ n) holds. Condition H^′′ : Condition H and

there exists a recursive functionh : N → Ns.t.

∀n∀X⊂_finB (|X| ≥ h(n) → |N(X)| − |X| ≥ n) holds. Theorem. (Kierstead, 1983)

B^′′_H′′G^′′M holds recursively. Theorem. (Kierstead, 1983) B^′′_H′G^′′M does not hold recursively.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 12 / 32

Facts (Review)

B^′_HGM holds. (Infinite marriage theorem) B_HGM does not hold.

Proposition. (Kierstead, 1983))

A bipartite graph(B, G; R)which satisfies condition H^′, has a solution. That is,B_H^′GM holds.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 13 / 32

The Strength of Marriage Theorems

H H

H

B_HGM B_H^′GM B_H^′′GM False BHG^′M BH^′G^′M BH^′′G^′M

B_HG^′′M B_H^′G^′′M B_H^′′G^′′M

ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL←^Hirst−−→ B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M

(nonrecursive) (recursive)

H

:

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 14 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ BH^′G^′′M BH^′′G^′′M

ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL←^Hirst−−→ B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀ (nonrecursive)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 15 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ BH^′G^′′M BH^′′G^′′M

ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL←^Hirst−−→ B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 16 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M

ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 17 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 18 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M ACA←^Hirst−−→ B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 19 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ B_H^′G^′M B_H^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M ACA B^′_HGM B^′_H′GM B^′_H′′GM

B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 20 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ BH^′G^′M BH^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M⊣RCA_0+Σ⁰₃-IND

ACA B^′_HGM B^′_H′GM B^′_H′′GM B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM

B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 21 / 32

The Strength of Marriage Theorems

H H

H

∗ B_H^′GM B_H^′′GM

∗ BH^′G^′M BH^′′G^′M

∗ B_H^′G^′′M B_H^′′G^′′M⊣RCA_0+Σ⁰₃-IND

ACA B^′_HGM B^′_H′GM B^′_H′′GM B^′_HG^′M B^′_H′G^′M B^′_H′′G^′M

B^′_HG^′′M B^′_H′G^′′M B^′_H′′G^′′M⊣RCA_0+Σ⁰₃-IND

WKL B^′′_HGM B^′′_H′GM B^′′_H′′GM B^′′_HG^′M B^′′_H′G^′M B^′′_H′′G^′M

B^′′_HG^′′M B^′′_H′G^′′M B^′′_H′′G^′′M⊣RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 22 / 32

The Strength of Marriage Theorems

Corollary. (RCA0+ Σ⁰₃^-IND⊢BH^′′G^′′M) B_H^′′G^′′M holds recursively.

Corollary. (RCA₀ ⊢ B^′′_H′′G^′M→ WKL) B^′′_H′′G^′M does not hold recursively. Theorem. (Kierstead, Review) B^′′_H′G^′′M does not hold recursively. Remark.

Condition H

and G

are essential to make marriage

theorem hold recursively.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 23 / 32

The Strength of Marriage Theorems

Corollary. (RCA0+ Σ⁰₃^-IND⊢BH^′′G^′′M) B_H^′′G^′′M holds recursively.

Corollary. (RCA₀ ⊢ B^′′_H′′G^′M→ WKL) B^′′_H′′G^′M does not hold recursively. Theorem. (Kierstead, Review) B^′′_H′G^′′M does not hold recursively. Remark.

Condition H

and G

are essential to make marriage

theorem hold recursively.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 23 / 32

On the Strength of Symmetric Marriage Theorems

B_HG_HM_s B_HG_H^′M_s B_HG_H^′′M_s B_H^′G_H^′M_s B_H^′G_H^′′M_s B_H^′′G_H^′′M_s B_HG^′_HM_s B_HG^′_H′M_s B_HG^′_H′′M_s B_H^′G^′_H′M_s B_H^′G^′_H′′M_s B_H^′′G^′_H′′M_s B_HG^′′_HM_s B_HG^′′_H′M_s B_HG^′′_H′′M_s B_H^′G^′′_H′M_s B_H^′G^′′_H′′M_s B_H^′′G^′′_H′′M_s B^′_HG_HM_s B^′_HG_H^′M_s B^′_HG_H^′′M_s B_H^′_′G_H^′M_s B^′_H′G_H^′′M_s B^′_H′′G_H^′′M_s B^′_HG^′_HM_s(Hirst) B^′_HG_H^′′M_s B^′_HG^′_H′′M_s B_H^′′G^′_H′M_s B^′_H′G_H^′′′M_s B^′_H′′G^′_H′′M_s B^′_HG^′′_HM_s B^′_HG_H^′′′M_s B^′_HG^′′_H′′M_s B_H^′′G^′′_H′M_s B^′_H′G_H^′′′′M_s B^′_H′′G^′′_H′′M_s B^′′_HG_HM_s B^′′_HG_H^′M_s B^′′_HG_H^′′M_s B_H^′′_′G_H^′M_s B^′′_H′G_H^′′M_s B^′′_H′′G_H^′′M_s B^′′_HG^′_HM_s B^′′_HG_H^′′M_s B^′′_HG^′_H′′M_s B_H^′′′G^′_H′M_s B^′′_H′G_H^′′′M_s B^′′_H′′G^′_H′′M_s B^′′_HG^′′_HM_s(Hirst) B^′′_HG_H^′′′M_s B^′′_HG^′′_H′′M_s B_H^′′′G^′′_H′M_s B^′′_H′G_H^′′′′M_s B^′′_H′′G^′′_H′′M_s

False ACA₀ WKL₀ RCA₀

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 24 / 32

Contents

1 What is Reverse Mathematics?

2 Previous Study on the Strength of Marriage Theorems.

3 Marriage Theorems with a lot of acquaintances.

4 Marriage Theorems with a few acquaintances.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 25 / 32

We consider a marriage theorem such that_{B = G = ω}. IM (Recasting of Infinite Marriage Theorem)

A bipartite graph(ω_B, ω_G; R)which satisfies condition H and

∀i, j∃t((i, j) ∈ R → j ≤ i + t), has a solution.

There exists a recursiveRsuch that_{G = (ω}B^{, ω}G; R)satisfies condition H and there exists a recursiveq : ω → ωs.t.

∀i, j((i, j) ∈ R → j ≤ i + q(i))holds, but does not have a recursive solution. (RCA₀ ⊢B^′′_HGM↔WKL (Hirst).) If q ≡ 0,{(i, i) | i ∈ ω}is a solution of^G, namely,^Ghas a recursive solution.

Where is the border?

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 26 / 32

We consider a marriage theorem such that_{B = G = ω}. IM (Recasting of Infinite Marriage Theorem)

A bipartite graph(ω_B, ω_G; R)which satisfies condition H and

∀i, j∃t((i, j) ∈ R → j ≤ i + t), has a solution.

There exists a recursiveRsuch that_{G = (ω}B^{, ω}G; R)satisfies condition H and there exists a recursiveq : ω → ωs.t.

∀i, j((i, j) ∈ R → j ≤ i + q(i))holds, but does not have a recursive solution. (RCA₀ ⊢B^′′_HGM↔WKL (Hirst).) If q ≡ 0,{(i, i) | i ∈ ω}is a solution of^G, namely,^Ghas a recursive solution.

Where is the border?

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 26 / 32

We consider a marriage theorem such that_{B = G = ω}. IM (Recasting of Infinite Marriage Theorem)

A bipartite graph(ω_B, ω_G; R)which satisfies condition H and

∀i, j∃t((i, j) ∈ R → j ≤ i + t), has a solution.

There exists a recursiveRsuch that_{G = (ω}B^{, ω}G; R)satisfies condition H and there exists a recursiveq : ω → ωs.t.

∀i, j((i, j) ∈ R → j ≤ i + q(i))holds, but does not have a recursive solution. (RCA₀ ⊢B^′′_HGM↔WKL (Hirst).) If q ≡ 0,{(i, i) | i ∈ ω}is a solution of^G, namely,^Ghas a recursive solution.

Where is the border?

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 26 / 32

We consider a marriage theorem such that_{B = G = ω}. IM (Recasting of Infinite Marriage Theorem)

A bipartite graph(ω_B, ω_G; R)which satisfies condition H and

∀i, j∃t((i, j) ∈ R → j ≤ i + t), has a solution.

There exists a recursiveRsuch that_{G = (ω}B^{, ω}G; R)satisfies condition H and there exists a recursiveq : ω → ωs.t.

∀i, j((i, j) ∈ R → j ≤ i + q(i))holds, but does not have a recursive solution. (RCA0 ^⊢B^′′_HGM↔WKL (Hirst).) If q ≡ 0,{(i, i) | i ∈ ω}is a solution of^G, namely,^Ghas a recursive solution.

We seeq : N → Nas a parameter, and investigate the strength of the following assertion IM(q)with respect to reverse mathematics.

IM(q): A bipartite graph(N_B, N_G; R)which satisfies condition H and ∀i, j((i, j) ∈ R → j ≤ i + q(i)), has a solution.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 26 / 32

Theorem.

1 _{RCA0 ⊢ q}is bounded by standard constant→IM(q).

2 _{RCA0+ Π}⁰

2^{-IND⊢qis bounded→IM(q).} 3 _{RCA0 ⊢ q}is unbounded and nondecreasing

→(IM(q) ↔ WKL).

IM(q): A bipartite graph(NB^{, N}G; R)which satisfies condition H and ∀i, j((i, j) ∈ R → j ≤ i + q(i)), has a solution. Corollary.

For any recursiveR ⊂ ω × ω andq : ω → ωwhich satisfies condition H and∀i, j ((i, j) ∈ R → j ≤ i + q(i))^,

G = (ωB^{, ω}G; R)has a recursive solution ifqis bounded. Gdoes not necessary have a recursive solution ifqis unbounded.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 27 / 32

Theorem.

1 _{RCA0 ⊢ q}is bounded by standard constant→IM(q).

2 _{RCA0+ Π}⁰

2^{-IND⊢qis bounded→IM(q).} 3 _{RCA0 ⊢ q}is unbounded and nondecreasing

→(IM(q) ↔ WKL).

IM(q): A bipartite graph(NB^{, N}G; R)which satisfies condition H and ∀i, j((i, j) ∈ R → j ≤ i + q(i)), has a solution. Corollary.

For any recursiveR ⊂ ω × ω andq : ω → ωwhich satisfies condition H and∀i, j ((i, j) ∈ R → j ≤ i + q(i))^,

G = (ωB^{, ω}G; R)has a recursive solution ifqis bounded. Gdoes not necessary have a recursive solution ifqis unbounded.

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 27 / 32

Theorem. (Recasting of RCA_{0+ Π}⁰₂-IND⊢ qis bounded→ IM(q)) RCA_{0+ Π}⁰₂-IND⊢IM^∗.

IM^∗: A bipartite graph(NB^{, N}G; R)which satisfies condition H and∃k∀i, j((i, j) ∈ R → j ≤ i + k), has a solution. WKL0 ^⊢IM^∗and RCA0+ Π⁰₂^{-IND⊢IM∗both hold.}

Question.

RCA0 ⁰ IM^∗? (RCA0 ^⊢IM^∗↔ WKL∨_Π⁰₂-IND ?)

Makoto Fujiwara (Tohoku University) Recursive Marriage Theorems and Reverse Mathematics 2012.2.21 28 / 32