ファイル置き場 Sendai Logic Homepage speaker11

Effective Strong Nullness and

Diminutiveness

Kojiro Higuchi

Joint work with Takayuki Kihara

Tohoku University

Wednesday 22, 2012

Strong Nullness

• Basic Notions:

• ω= {0, 1, 2, 3, · · · }, ω^ω = {f | f : ω → ω}.

• ω^<ω is the set of all (finite) strings.

• For a string σ ∈ ω^<ω, [[σ]] = {f ∈ ω^ω | f ⊃ σ}.

• A set P ⊂ ω^ω is null iff (∀ k ∈ ω)(∃ {σⁿ}n∈ω ⊂ ω^<ω)

[P ⊂^∪_n∈ω[[σn]] & ^∑_n∈ω1/2^lh(σn)≤ 1/2^k].

• A set P ⊂ ω^ω is strongly nulliff (∀ {kn}n∈ω ⊂ ω)(∃ {σn}n∈ω ⊂ ω^<ω)

[P ⊂^∪_n∈ω[[σn]] & (∀n)[1/2^lh(σn) ≤ 1/2^kn]].

Strong Nullness

• Basic Notions:

• ω= {0, 1, 2, 3, · · · }, ω^ω = {f | f : ω → ω}.

• ω^<ω is the set of all (finite) strings.

• For a string σ ∈ ω^<ω, [[σ]] = {f ∈ ω^ω | f ⊃ σ}.

• A set P ⊂ ω^ω is null iff (∀ k ∈ ω)(∃ {σⁿ}n∈ω ⊂ ω^<ω)

[P ⊂^∪_n∈ω[[σn]] & ^∑_n∈ω1/2^lh(σn)≤ 1/2^k].

• A set P ⊂ ω^ω is strongly nulliff (∀ {kn}n∈ω ⊂ ω)(∃ {σn}n∈ω ⊂ ω^<ω) [P ⊂^∪_n∈ω[[σn]] & (∀n)[lh(σn) ≥ kn]].

Background

• In 1919, Borel introduced strong nullness on the subsets of R.

• He conjectured that every strong null set of reals is countable. (Borel Conjecture)

• In 1928, Sierpi´nski proved that ZFC+CH ⊢ ¬BC.

• In 1976, Laver proved that BC is independent of ZFC.

Effective Strong Nullness

• A set P ⊂ ω^ω is strongly nulliff (∀ {kn}n∈ω ⊂ ω)(∃ {σn}n∈ω ⊂ ω^<ω) [P ⊂^∪_n∈ω[[σn]] & (∀n)[lh(σn) ≥ kn]].

• A set P ⊂ ω^ω is effectively strongly nulliff (∀ computable {kn}_n∈ω ⊂ ω)(∃ {σn}_n∈ω ⊂ ω^<ω) [P ⊂^∪_n∈ω[[σⁿ]] & (∀n)[lh(σⁿ) ≥ kⁿ]].

• 2^ω = {f | f : ω → {0, 1}}.

• We will characterize effective strong nullness for closed subsets of 2^ω.

• Recall that P ⊂ 2^ω is closed iff (∃ a tree TP ⊂ 2^<ω)[ P = [TP] ],

where [TP] is the set of all paths through TP.

···

P

}

TP

• Thm. For a closed subset P of 2^ω,

P is not effectively strongly null

⇐⇒ P contains a computably perfect subset.

• A closed set Q ⊂ ω^ω iscomputably perfect iff (∃ computable F : ω → ω)(∀f ∈ Q)(∀n) [ (Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅ ].

n F(n)

A Proof of ⇐

• Q _is computably perfectiff (∃ computable F ) (∀f ∈ Q)(∀n)[(Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅].

• P is not effectively strongly null iff

(∃ computable {kn}_n∈ω ⊂ ω)(∀ {σn}_n∈ω ⊂ ω^<ω) [(∀n)[lh(σⁿ) ≥ kⁿ] =⇒ P ̸⊂^∪_n∈ω[[σⁿ]]].

• A closed P ⊂ 2^ω contains a computably perfect subset Q

=⇒ P is not effectively strongly null.

0

k_{0 = F (0)} k_{1 = FF (0)} k₂ = FFF (0)^··

·

A Proof of ⇐

• Q _is computably perfectiff (∃ computable F ) (∀f ∈ Q)(∀n)[(Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅].

• P is not effectively strongly null iff

(∃ computable {kn}_n∈ω ⊂ ω)(∀ {σn}_n∈ω ⊂ ω^<ω) [(∀n)[lh(σⁿ) ≥ kⁿ] =⇒ P ̸⊂^∪_n∈ω[[σⁿ]]].

• A closed P ⊂ 2^ω contains a computably perfect subset Q

=⇒ P is not effectively strongly null.

0

k_{0 = F (0)} k_{1 = FF (0)} k₂ = FFF (0)

σ0

•

···

A Proof of ⇐

• Q _is computably perfectiff (∃ computable F ) (∀f ∈ Q)(∀n)[(Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅].

• P is not effectively strongly null iff

(∃ computable {kn}_n∈ω ⊂ ω)(∀ {σn}_n∈ω ⊂ ω^<ω) [(∀n)[lh(σⁿ) ≥ kⁿ] =⇒ P ̸⊂^∪_n∈ω[[σⁿ]]].

• A closed P ⊂ 2^ω contains a computably perfect subset Q

=⇒ P is not effectively strongly null.

0

k_{0 = F (0)} k_{1 = FF (0)} k₂ = FFF (0)

σ0

•

σ1

•

···

A Proof of ⇐

• Q _is computably perfectiff (∃ computable F ) (∀f ∈ Q)(∀n)[(Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅].

• P is not effectively strongly null iff

(∃ computable {kn}_n∈ω ⊂ ω)(∀ {σn}_n∈ω ⊂ ω^<ω) [(∀n)[lh(σⁿ) ≥ kⁿ] =⇒ P ̸⊂^∪_n∈ω[[σⁿ]]].

• A closed P ⊂ 2^ω contains a computably perfect subset Q

=⇒ P is not effectively strongly null.

0

k_{0 = F (0)} k_{1 = FF (0)} k₂ = FFF (0)

σ0

•

σ1

•

σ2

•

···

A Proof of ⇐

• Q _is computably perfectiff (∃ computable F ) (∀f ∈ Q)(∀n)[(Q ∩ [[f ↾ n]]) \ [[f ↾ F (n)]] ̸= ∅].

• P is not effectively strongly null iff

(∃ computable {kn}_n∈ω ⊂ ω)(∀ {σn}_n∈ω ⊂ ω^<ω) [(∀n)[lh(σⁿ) ≥ kⁿ] =⇒ P ̸⊂^∪_n∈ω[[σⁿ]]].

• A closed P ⊂ 2^ω contains a computably perfect subset Q

=⇒ P is not effectively strongly null.

0

k_{0 = F (0)} k_{1 = FF (0)} k₂ = FFF (0)

σ0

•

σ1

•

σ2

•

···

Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

T ⁰

1

··· 2

Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

T ⁰

1 2

A

A ^··

·

Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

T ⁰

1 2

A

A ^··

·

Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

T ⁰

1

··· 2

Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

T ⁰

1 2

T^′

···

A Proof of Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• ^Ext(T ) = {σ ∈ T | (∃f ∈ [T ])[ σ ⊂ f ]}.

• ^Br(T ) = {σ ∈ T | (∃n ̸= m)[ σn, σm ∈ Ext(T ) ]}.

• Let T be the set of all finitely branching subtree T of ω^<ω such that Ext(T ) \ Br(T ) ̸= ∅.

•

•

•

•

•

•

•

•

•

•

•

•

•

•

• •

•

···

A Proof of Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• ^Ext(T ) = {σ ∈ T | (∃f ∈ [T ])[ σ ⊂ f ]}.

• ^Br(T ) = {σ ∈ T | (∃n ̸= m)[ σn, σm ∈ Ext(T ) ]}.

• Let T be the set of all finitely branching subtree T of ω^<ω such that Ext(T ) \ Br(T ) ̸= ∅.

•

• Ext_{(T )}

•

•

•

•

•

•

•

•

•

•

•

•

• •

•

···

A Proof of Combinatorial Theorem

• Let T ⊂ ω^<ω be a finitely branching tree.

• ^Ext(T ) = {σ ∈ T | (∃f ∈ [T ])[ σ ⊂ f ]}.

• ^Br(T ) = {σ ∈ T | (∃n ̸= m)[ σn, σm ∈ Ext(T ) ]}.

• Let T be the set of all finitely branching subtree T of ω^<ω such that Ext(T ) \ Br(T ) ̸= ∅.

•

• Br_{(T )}

•

•

•

•

•

•

•

•

•

•

•

•

• •

•

···

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (1)

• Let c : T → ω^<ω such that c(T ) = σn with σn ∈ Ext(T ) and σ ̸∈ Br(T ) for all T ∈ T.

• Given a finitely branching T ⊂ ω^<ω, define T0 = Ext(T ) and Tα = Ext(^∩_β<α(Tβ\ {σ | σ ⊃ c(Tβ)}) for all α > 0. Here, we understand Tα+1 = Tα if Ext(Tα) \ Br(Tα) = ∅.

• Let α0 be the least fixed point ordinal of {Tα}α.

• Then (∀σ ∈ Tα0)(∃n ̸= m)[σn, σm ∈ Tα0^].

• For β < α₀, let c(Tβ) = σβⁿβ.

• For β < γ < α0, we have σβ ̸= σγ since σγ ∈ Tγ⊂ Ext(Tβ \ {σ | σ ⊃ c(Tβ)}) ̸∋ σβ.

• Thus, β 7→ σβ is injective.

A Proof of Combinatorial Theorem (2)

• We want to show that for an f.b. tree T ⊂ ω^<ω, [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

• Define A = {c(Tβ) | β < α₀}.

• Since c(Tβ) = σβⁿβ 7→ σβ is injective, we have [Tα0^{] = [T ] \}

∪

σ∈A[[σ]] ̸= ∅.

Thus T^′ = Tα0 satisfies the desired property.

A Proof of Combinatorial Theorem (2)

• We want to show that for an f.b. tree T ⊂ ω^<ω, [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

• Define A = {c(Tβ) | β < α₀}.

• Since c(Tβ) = σβⁿβ 7→ σβ is injective, we have [Tα0^{] = [T ] \}

∪

σ∈A[[σ]] ̸= ∅.

Thus T^′ = Tα0 satisfies the desired property.

A Proof of Combinatorial Theorem (2)

• We want to show that for an f.b. tree T ⊂ ω^<ω, [(∀A ⊂ T \ {∅})

[(∀n)[#(A∩ωⁿ⁺¹) ≤ #(T ∩ωⁿ)] =⇒ [T ]\^∪_σ∈A[[σ]] ̸= ∅]]

=⇒

(∃ nonempty T^′ ⊂ T )(∀σ ∈ T^′)(∃n ̸= m)[σn, σm ∈ T^′].

• Define A = {c(Tβ) | β < α₀}.

• Since c(Tβ) = σβⁿβ 7→ σβ is injective, we have [Tα0^{] = [T ] \}

∪

σ∈A[[σ]] ̸= ∅.

Thus T^′ = Tα0 satisfies the desired property.

A Proof of ⇒

Now we show that

• A closed P ⊂ 2^ω is not effectively strongly null

=⇒ P contains a computably perfect subset.

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

kG₍₀₎

kG₍₁₎

kG₍₂₎

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

kG₍₀₎

kG₍₁₎

kG₍₂₎

A A

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

•

•

•

•

σG₍₀₎, . . . , σG₍₁₎₋₁

σG₍₁₎, . . . , σG₍₂₎₋₁

kG₍₀₎

kG₍₁₎

kG₍₂₎

A A

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

•

•

•

•

σG₍₀₎, . . . , σG₍₁₎₋₁

σG₍₁₎, . . . , σG₍₂₎₋₁

kG₍₀₎

kG₍₁₎

kG₍₂₎

A A

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

kG₍₀₎

kG₍₁₎

kG₍₂₎

A Proof of ⇒

• Suppose that P isnot effectively strongly null, i.e., (∃ computable {kn}n∈ω ⊂ ω)(∀ {σn}n∈ω ⊂ ω^<ω) [(∀n)[lh(σn) ≥ kn] =⇒ P ̸⊂^∪_n∈ω[[σn]]].

• We can assume kn < kn₊₁ for all n ∈ ω.

• Define G by G (0) = 0, G (n + 1) = G (n) + 2^G(n).

kG₍₀₎

kG₍₁₎

kG₍₂₎

Futher Characterizations

• For a closed subset P of 2^ω, the following are equivalent:

• P is effectively strongly null.

• P contains no computably perfect subset (i.e., P is diminutive).

• Thm(Binns). For a nonempty Π⁰₁ subsets of 2^ω, TFAE:

• P is diminutive.

• There is f ∈ 2^ω wtt-reducible to no element in P.

• P contains no complex element.

Here, f ∈ 2^ω is complex if there is a computable function G such that for all n ∈ ω, K (f ↾ G (n)) ≥ n holds,

where K is the prefix-free complexity.

Futher Characterizations

• For a closed subset P of 2^ω, the following are equivalent:

• P is effectively strongly null.

• P contains no computably perfect subset (i.e., P is diminutive).

• Thm(Binns). For a nonempty Π⁰₁ subsets of 2^ω, TFAE:

• P is diminutive.

• There is f ∈ 2^ω wtt-reducible to no element in P.

• P contains no complex element.

Here, f ∈ 2^ω is complex if there is a computable function G such that for all n ∈ ω, K (f ↾ G (n)) ≥ n holds,

where K is the prefix-free complexity.

Below WKL

• Let ϕ(T ) be a formula.

• We write WKL(ϕ) for the statement:

Every infinite binary tree T which satisfies ϕ has a path.

• For instance, WKL(µ([T ]) > 0) ≡ WWKL.

Below WKL

• Consider the following statements:

• DIM(T ) ≡ [T ] is “diminutive”.

• VS(T ) ≡ [T ] is “very small”, i.e.,

(∀F : N → N)(∃^∞n∈ N)[#(Ext(T ) ∩ 2^F(n)) < n].

• SN(T ) ≡ [T ] is “strong null”.

• Theorem (Binns and Kjos-Hanssen).

RCA₀ WKL

WKL(VS)

WKL(DIM) _WWKL

DNR

Below WKL

• Consider the following statements:

• DIM(T ) ≡ [T ] is “diminutive”, i.e.,

¬(∃ nonempty tree T^′⊂ T )(∃F : N → N)(∀n ∈ N) (∀σ ∈ Ext(T^′)∩2ⁿ)(∃τ₀̸= τ1∈ 2^F(n))[τ₀, τ₁ ∈ Ext(T^′)].

• SN(T ) ≡ [T ] is “strong null”, i.e.,

(∀F : N → N)(∃n)(∃{σm_}m<n)[(∀m < n)[lh(σm) ≥ F(m)] & [T ] ⊂^∪_m<n[[σm]]].

• Prop. RCA0 ⊢WKL(DIM) ⇐⇒ WKL(SN).

• There may be a “natural” mathematical statement which is equivalent to WKL(ϕ) over RCA0 for some smallness property ϕ(T ) of trees.

• However, the following facts hold:

• (ω, P(ω)) |= [T ] is finite if T is a very small infinite tree.

• (Laver) ZFC̸⊢ “(ω, P(ω)) |= There exists an infinite diminutive tree with uncountably many paths.”

Closure Properties

• Let A = {P ⊂ 2^ω | P is nonempty diminutive Π⁰₁ set }.

• Thm. The following hold:

• Ais closed under taking nonempty Π⁰₁ subsets.

• Ais closed under taking images of computable functions.

• For P, Q ⊂ ω^ω, P ≤^{w Q} iff ∀g ∈ Q ∃f ∈ P ^f ≤T g_.

• Let MLR and DNR denote the set of all Martin-L¨of random sets and all diagonally non-recursive functions, respectively.

• Thm. Suppose that nonempty Π⁰₁ sets P, Q ⊂ 2^ω and a set B of nonempty Π⁰₁ subsets of 2^ω satisfy:

• P, Q contain no computable element and P ≤w ^MLR.

• Q _{∈ B and P}^′ ̸∈ B for any nonempty Π⁰₁ set P^′ ⊂ P.

• Bis closed under taking nonempty Π⁰₁ subsets and taking images of computable functions.

Then P ̸≤^{w Q} and P ̸≥^{w Q}.

• Theorem (Binns). A nonempty Π⁰₁ set P^′ is not diminutive if P^′ ≥^{w DNR}.

• Cor. P ̸≤^w Q and P ̸≥^w Q for any nonempty Π⁰₁ sets P, Q ⊂ 2^ω with no computable element such that DNR_{≤w P ≤w} MLR _{and Q ∈ A.}

• Thm. Given a formula ϕ(T ), consider the set

B= {[T ] | T is an infinite tree & ϕ(T )}. Suppose that a nonempty Π⁰₁ sets P ⊂MLR and B satisfy:

• There is P ∈ B with no computable element.

• P^′̸∈ B for any nonempty Π⁰₁ set P^′ ⊂ P.

• Bis closed under taking nonempty Π⁰₁ subsets and taking images of computable functions.

Then RCA0+WWKL ̸⊢ WKL(ϕ).

Thank you!