This story draft by @escholar has not been reviewed by an editor, YET.
Authors:
(1) Laurent Bienvenu;
(2) Christopher P. Porter.
4 Members of Deep Π0 1 classes
Working towards the proof of Lemma 3, we first establish the following result.
We thus have the identity
Then by our initial assumption on t and t′, we have
The lemma follows by taking the negative logarithm of this inequality
We can now prove Lemma 3. The (i)→(ii) implication is immediate. For the (ii)→(i) implication, suppose X is a sequence and h a computable increasing function such that
for any time bound t. If k ∈ [h(n), h(n + 1)), we have
We now apply the previous lemma with σ = X↾h(n), τ = X↾[h(n), k) and E the map such that, on input ρ, checks whether ρ has length h(n) for some n and if so returns all strings whose length is between 0 and h(n + 1) − h(n) (otherwise E(ρ) is empty). The lemma gives us a computable time bound s such that
This being true for all n and all k ∈ [h(n), h(n + 1)), we have
and thus X is order-deep.
Finally, the (ii)↔(iii) equivalence can be established using Lemma 1(iii) and Theorem 2.
This paper is available on arxiv under CC BY 4.0 DEED license.