This paper investigates whether an analogue of ATR_0 exists in the Weihrauch lattice, exploring various candidates and highlighting the complexity of establishing such a correspondence.
Contribution
It systematically evaluates potential counterparts of ATR_0 in the Weihrauch degrees, revealing the challenges and intricacies involved.
Findings
01
Multiple candidates for ATR_0 analogue are considered.
02
No definitive counterpart for ATR_0 is identified.
03
The relationship between reverse mathematics and Weihrauch degrees is complex.
Abstract
There are close similarities between the Weihrauch lattice and the zoo of axiom systems in reverse mathematics. Following these similarities has often allowed researchers to translate results from one setting to the other. However, amongst the big five axiom systems from reverse mathematics, so far ATR_0 has no identified counterpart in the Weihrauch degrees. We explore and evaluate several candidates, and conclude that the situation is complicated.
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Full text
Searching for an analogue of ATR0
in the Weihrauch lattice
Takayuki Kihara
Department of Mathematical Informatics
Nagoya University, Nagoya, Japan
[email protected]
Dipartimento di Scienze Matematiche, Informatiche e Fisiche
Universitá di Udine, Udine, ItalyDepartment of Computer Science
Swansea University, Swansea, UK
&
Department of Computer Science
University of Birmingham, Birmingham, UK
Alberto Marcone
Dipartimento di Scienze Matematiche, Informatiche e Fisiche
Universitá di Udine, Udine, Italy
[email protected]
Department of Computer Science
There are close similarities between the Weihrauch lattice and the zoo of
axiom systems in reverse mathematics. Following these similarities has
often allowed researchers to translate results from one setting to the
other. However, amongst the big five axiom systems from reverse
mathematics, so far ATR0 has no identified counterpart in the
Weihrauch degrees. We explore and evaluate several candidates, and conclude
that the situation is complicated.
1 Introduction
Reverse mathematics [43] is a program to find the sufficient
and necessary axioms to prove theorems of mathematics (that can be formalized
in second-order arithmetic). For this, a base system (RCA0) is
fixed, and then equivalences between theorems and certain benchmark axioms
are proven. Sometimes, a careful reading of the original proof of the theorem
reveals which of the benchmark axioms are used, and the main challenge is to
show that the theorem indeed implies those axioms (hence the name
reverse mathematics). A vast number of theorems turned out to be
equivalent to one of only five systems: RCA0, WKL0,
ACA0, ATR0 and Π11\mbox−CA0. While
recently attention has shifted to theorems not equivalent to one of the
big five, the big five still occupy a central role in the endeavour.
Computational metamathematics in the Weihrauch lattice starts with the
observation that many theorems in analysis and other areas of mathematics
have Π2-gestalt, i.e. are of the form ∀x∈X(Q(x)→∃y∈YP(x,y)), and can hence be seen
as computational tasks: Given some x∈X satisfying Q(x), find
a suitable witness y∈Y. This task can also be viewed as a
multivalued partial function f:⊆X⇉Y, and
thus the precise definition of Weihrauch reducibility (given in
§2.2 below) deals with this kind of objects. Often, the task
cannot be solved algorithmically (equivalently, the multivalued function is
not computable). The research programme (as formulated by Gherardi and
Marcone [21], Pauly [36, 38] and in particular Brattka and Gherardi [8, 7]) is
to compare the degree of impossibility as follows: Assume we had a black box
to solve the task for Theorem B. Can we solve the task for Theorem A using
the black box exactly once? If so, then A≤WB, A is Weihrauch
reducible to B.
As provability in RCA0 is closely linked to computability, it is
maybe not that surprising that very often, classification in reverse math can
be translated easily into Weihrauch reductions111The reverse direction
would also be possible, but as reverse mathematics is the older field, occurs
seldom in practice.. While there are a number of obstacles for precise
correspondence (see [25] for a detailed discussion), the
resource-sensitivity of Weihrauch reductions might be the most obvious one: A
proof in reverse mathematics can use a principle multiple times, a Weihrauch
reduction uses its black box once. This obstacle does not apply to
RCA0 or WKL0 classifications.
The analogue of RCA0 are the computable principles, the analogue
of WKL0 is C2N (closed choice on Cantor space), and the
analogue of ACA0 is lim or finite iterations thereof.
Theorems equivalent to Π11\mbox−CA0 have not yet been studied
in the Weihrauch lattice, but an obvious analogue of
Π11\mbox−CA0 is readily defined as the function which maps a
countable sequence of trees to the characteristic function of the set of
indices corresponding to well-founded trees. This leaves ATR0 out
of the big five, leading Marcone to initiate the search for an analogue in
the Weihrauch lattice at a Dagstuhl meeting on Weihrauch reducibility
[14].
Two candidates have been put forth as potential answers, UCNN and
CNN (unique choice and closed choice on Baire space). We will examine
some evidence for both of them, and show that the question is not as easily
answered as those for the other big five. Our main focus is on three
particular theorems equivalent to ATR0 in reverse mathematics:
Comparability of well orderings, open determinacy on Baire space222The
version for Cantor space has been studied in the Weihrauch degrees by Le Roux
and Pauly [31]. and the perfect tree theorem.
Theorem** (Comparability of well orderings).**
If X and Y are well orderings over N, then ∣X∣≤∣Y∣ or ∣Y∣≤∣X∣.
Theorem** (Open determinacy).**
Consider a two-player infinite sequential game with moves from N. Let the
first player have an open winning set. Then one player has a winning
strategy.
Theorem** (Perfect Tree Theorem).**
If T⊆N<N is a tree, then either [T] is countable or T
has a perfect subtree.
Structure of the paper
In Section 2 we recall the prerequisite notions about
Weihrauch reducibility. While reverse mathematics serves as the motivation
for this paper, its results are not invoked in our proofs, hence we do not
expand on this area. In Section 3 we recall two Weihrauch
degrees of central importance, unique choice UCNN and closed choice
CNN on Baire space. We then prove some equivalences to those for
variants of comprehension and separation principles. In Section
4, we re-examine the strength of a separation principle,
which is shown to be equivalent to Σ11-WKL, weak König’s lemma for
Σ11-trees (Theorem 4.3). The comparability of
well orderings is studied in Section 5. We see two
variants, one of which we prove to be equivalent to UCNN (Theorem
5.5) whereas the other resists full classification (Question
5.8).
Open determinacy and the perfect tree theorem are investigated in Sections
6 and 7. Both principles are formulated as
disjunctions, and the versions where we know in which case we are are proven
to be equivalent to UCNN or CNN in Section 6.
The results about open determinacy can be seen as uniform versions of the
study of the complexity of winning strategies in [3]. If
no case is fixed, we arrive at Weihrauch degrees not previously studied. Some
of their properties are exhibited in Section 7. Since the
degrees studied in Section 7 are not very well behaved, we
introduce the canonical principle TCNN, the total continuation of
closed choice in Section 8. We prove that up to finite
parallelization, it is equivalent to the two-sided versions of open
determinacy and the perfect tree theorem, and show some additional properties
of the degree. Some concluding remarks and open questions are found in
Section 9.
The following illustrates the strength of key benchmark principles in this article:
[TABLE]
2 Background on represented spaces and Weihrauch degrees
For background on the theory of represented spaces we
refer to [39], for an introduction to and survey of
Weihrauch reducibility we point the reader to [13].
As usual in the area, we use angle brackets to denote a variety of pairing
and coding functions, such as those from N×N to N, from
N<N to N, and from NN×NN, (NN)<N and
(NN)N to NN. The context provides information about the one
actually employed in any given instance.
2.1 Represented spaces
Definition 2.1**.**
A represented spaceX is a set X together with a partial
surjection δX:⊆NN→X. If x∈X, any
element of (δX)−1(x) is called a name or a
code for x.
A partial function F:⊆NN→NN is called a realizer
of a function f:⊆X→Y between represented
spaces, if f(δX(p))=δY(F(p)) holds for all
p∈dom(f∘δX). We denote F being an realizer of
f by F⊢f. We then call f:⊆X→Ycomputable (respectively continuous), iff it has a computable
(respectively continuous) realizer.
Represented spaces can adequately model most spaces of interest in
everyday mathematics. For our purposes, we only need a few specific
spaces that we discuss in the following, as well as some constructions of
hyperspaces.
The category of represented spaces and continuous functions is
cartesian-closed, by virtue of the UTM-theorem. Thus, for any two represented
spaces X, Y we have a represented space
C(X,Y) of continuous functions from
X to Y. The expected operations involving
C(X,Y) (evaluation, composition, (un)currying)
are all computable. Using the Sierpiński space S with underlying
set {⊤,⊥} and representation δS:NN→{⊤,⊥} defined via δS(⊥)−1={0ω},
we can then define the represented space O(X) of
open subsets of X by identifying a subset of X
with its (continuous) characteristic function into S. Since
countable or and binary and on S are computable, so
are countable union and binary intersection of open sets. The space
A(X) of closed subsets is obtained by taking formal
complements, i.e. the names for A∈A(X) are the same
as the names of X∖A∈O(X) (i.e. we are
using the negative information representation).
We indicate with Tr the space of trees on N represented in an obvious
way via characteristic functions on the set of finite sequences. The
computable map []:Tr→A(NN) maps a tree to its set of
infinite paths, and has a computable multivalued inverse. In other words, one
can compute a code of a tree T from a code of a closed set [T], and vice
versa.
Given a represented space X and k∈N, using Borel codes, the
collections Σk0(X) (respectively Πk0(X)) of Σk0
(respectively Πk0) subsets of X can be naturally viewed as a
represented space, cf. [4, 23, 40]. Equivalently, we can
use the jumps of S to characterize these spaces. We find that
A and Π10 (respectively O and Σ10) are
identical.
The collection Σ11(X) of analytic subsets of X can
also be represented in a straightforward manner: p is a name of a Σ11
set S⊆X iff p is a name of a closed set
P⊆NN×X such that S={x∈X:(∃g)(g,x)∈P}. Equivalently ([41, Proposition
35]), we can define the space SΣ11
by letting it have the underlying set {⊤,⊥}, and letting p∈NN be a name for ⊤ iff the tree on N coded by p is ill-founded;
and then identify Σ11(X) with
C(X,SΣ11) (here f∈C(X,SΣ11) represents the
Σ11(X) set f−1(⊤)). Again, the collection
Π11(X) of coanalytic subsets of X is represented in
an obvious way by taking formal complements. We define the space
SΠ11 with underlying set {⊤,⊥}, so that p∈NN is a name for ⊤ iff the tree on N coded by p is well-founded.
We first check that basic operations on these represented spaces are
well-behaved.
Lemma 2.2**.**
The following operations are computable:
⋁,⋀:SΣ11N→SΣ11
2. 2.
∃:Σ11(X)→SΣ11, mapping
non-empty sets to ⊤ and the empty set to ⊥.
3. 3.
id,¬:S→SΣ11
Proof.
For ⋁, we need to show that given a sequence of trees we can compute a tree that is ill-founded iff one of the contributing trees is. This can be done by simply joining them at the root. For ⋀, we need a tree that is ill-founded iff all them are. For that, we can take the product of the trees (e.g. as in [35]).
2. 2.
From f∈C(NN,SΣ11) we can compute by
type-conversion some g:NN×NN→S such that
f(p)=⊤ iff ∃q∈NNg(p,q)=⊥. But then
∃p∈NNf(p)=⊤⇔∃⟨p,q⟩∈NNg(p,q)=⊥, and we are done.
3. 3.
For ¬:S→SΣ11, given a name p for a
point in S let the tree T be defined by w∈T iff
∀n≤∣w∣p(n)=0. For id:S→SΣ11, we let T have only branches of the form
n0ω, and such a branch is present iff p(n)=0.∎
Proposition 2.3**.**
The following operations are computable for any represented space
X and k>0:
(1-6) These all follow directly from Lemma 2.2 together with function composition.
(7) It is well-known that a∈NN is hyperarithmetical relative to
{a}∈Π10(NN) (cf. Corollary 3.3 and
accompanying remarks below). The section map (x,C)↦{y∈NN∣(y,x)∈C}:X×Π10(NN×X)→Π10(NN) is computable, see [39, Proposition 4.2 (9)].
Thus, we find that
[TABLE]
The first set on the right-hand side is Π11 by Kleene’s
HYP-quantification theorem [28, 29] (see also [42, Lemma III.3.1]); that is, the formula ∃y∈HYP(x)P(x,y) means that there are natural numbers a,e such that a∈Ox (which represents an ordinal α) and the e-th real Φe(x(α)) computable in the α-th Turing jump of x satisfies P(x,Φe(x(α))), where Ox is Kleene’s system of ordinal notations relative to x (which is a Π11(x) set), cf. [42].
This description is trivially Π11, uniformly relative to x and the complexity of P,
so that we can actually compute the Π11 set from C. The second set
explicitly and uniformly defines a Π11 set. The claim thus follows using
that intersection is a computable operation on Π11 sets from (2).
∎
Lemma 2.4**.**
Let X be a represented space. Then the function
F:⨆kΠk0(NN×X)→Σ11(X)
defined by
[TABLE]
is computable.
Proof.
Proposition 2.3(5) is typically proved by induction on k,
and the inductive argument is uniform in k. Since (a name for) for B∈⨆kΠk0(NN×X) includes the information about the
k such that B∈Πk0(NN×X), we can uniformly repeat
k steps of the induction argument to obtain a name for {x∈X:∃g∈NN(g,x)∈B} as a Σ11(X) set.
∎
We define the represented spaces LO and WO respectively of linear
orderings and countable well orderings with domain contained in N (thus
WO is a subspace of LO) as follows: p is a name for the linear order
(X,⪯X) with X⊆N if p(⟨n,m⟩)=1 if
and only if n⪯Xm. We often abuse notation by leaving ⪯X
implicit and writing X∈LO. We may assume without loss of generality
that, for all X∈LO, 0∈/X (this will be useful in Definition
5.1 below). If X∈LO we use interchangeably WO(X) and X∈WO. If X∈WO we indicate its order type by ∣X∣. Given some tree
T⊆N<N, we define the Kleene-Brouwer ordering
⪯KB on T as the transitive closure of w⪯KBu if w⊒u and un⪯KBum if n≤m. Using
the coding of finite strings we view (T,⪯KB) as a member
of LO.
Observation 2.5**.**
The map KB:Tr→LO mapping a tree to
its Kleene-Brouwer ordering is computable. We have WO(KB(T)) iff T
is well-founded.
We need a technical definition, which can be found in [43, Definition
V.6.4], for some of our proofs related to well orderings.
Definition 2.6** (double descent tree).**
If X,Y∈LO the double descent treeT(X,Y) is the set of
all finite sequences of the form ⟨(m0,n0),(m1,n1),…,(mk−1,nk−1)⟩∈N<N such that
•
m0,m1,…,mk−1∈X and m0>Xm1>X⋯>Xmk−1,
•
n0,n1,…,nk−1∈Y and n0>Yn1>Y⋯>Ynk−1.
We define the linear ordering X∗Y=KB(T(X,Y)).
Observation 2.7**.**
(X,Y)↦(X∗Y):LO×LO→LO is computable.
With an abuse of notation, we use Q and N to denote respectively a
computable presentation of the standard linear ordering of rational numbers
and of the well ordering of natural numbers.
Lemma 2.8**.**
Let X,Y∈LO.
If WO(X) then X∗Y and Y∗X are well orderings.
2. 2.
If WO(X) and ¬WO(Y), then ∣X∣≤∣X∗Y∣.
3. 3.
If WO(Y), then ∣X∗Y∣≤∣Q∗Y∣.
Proof.
The proofs of 1 and 2 can be found in Lemma V.6.5 of [43]. In order to prove 3, consider a function g:X→Q such that, for all x,x′∈X,
(a)
x<Xx′→g(x)<Qg(x′),
2. (b)
x<Nx′→g(x)<Ng(x′).
It is easy to see that such a function exists. Define then g^:(X∗Y)→(Q∗Y) by putting g^(⟨(x0,y0),…,(xk−1,yk−1)⟩):=⟨(g(x0),y0),…,(g(xk−1),yk−1))⟩. Property a. of g guarantees that g^ is well-defined and property b. implies that g^ respects the Kleene-Brouwer orderings of the double descent trees X∗Y and Q∗Y.
∎
2.2 Weihrauch reducibility
Intuitively, f being Weihrauch reducible to g means that there is an
otherwise computable procedure to solve f by invoking an oracle for g
exactly once. We thus obtain a very fine-grained picture of the relative
strength of partial multivalued functions. Consequently, a Weihrauch
equivalence is a very strong result compared to other approaches that allow
more generous access to the principle being reduced to.
Definition 2.9** (Weihrauch reducibility).**
Let f,g be multivalued functions on represented
spaces. Then f is said to be Weihrauch reducible to g, in symbols
f≤Wg, if there are computable functions K,H:⊆NN→NN such
that (p↦K⟨p,GH(p)⟩)⊢f for all G⊢g.
If there are computable functions K,H:⊆NN→NN such that KGH⊢f for all G⊢g, then f is strongly Weihrauch
reducible to g, in symbols f≤sWg.
The relations ≤W, ≤sW are reflexive and transitive. We use ≡W (≡sW) to denote equivalence
and by <W we denote strict reducibility. Both Weihrauch degrees [37] and strong Weihrauch degrees [18] form lattices, the former being distributive and the latter not (in general, Weihrauch degrees behave more naturally than strong Weihrauch degrees).
Rather than the lattice operations, we will use two kinds of products in this
work: The parallel product f×g is just the usual cartesian product
of (multivalued) functions, which is readily seen to induce an operation on
(strong) Weihrauch degrees. We call f a cylinder, if f≡sW(idNN×f), and note that for cylinders, Weihrauch reducibility and
strong Weihrauch reducibility coincide.
The compositional product f⋆g satisfies that
[TABLE]
and thus is the hardest problem that can be realized using first g, then something computable, and finally f. The existence of the maximum is shown in [16]. Both products as well as the lattice-join can be interpreted as logical and, albeit with very different properties. The sequential product ⋆ is not commutative, however, it is the only one that admits a matching implication [16, 24].
Two further (unary) operations on Weihrauch degrees are relevant for us,
finite parallelization f∗ and parallelization f. The former
has as input a finite tuple of instances to f and needs to solve all of
them, the latter takes and solves a countable sequences of instances. Both
operations are closure operators in the Weihrauch lattice. They can be used
to relax the requirement of using the oracle only once, if so desired, by
looking at the relevant quotient lattices.
In passing, we will refer to the third operation, the jump from [12] (studied further in [5], denoted by f′. We use f(n) to denote the result of applying the jump n-times. The jump only preserves strong Weihrauch degrees. The input to f′ is a sequence converging (with unknown speed) to an input of f, the output is whatever f would output on the limit.
The well-studied Weihrauch degrees most relevant for us are unique closed
choice and closed choice (on Baire space), to which we dedicate the following
Section 3. Two other degrees we will refer to are LPO:NN→{0,1} and lim:⊆(NN)ω→NN. These are
defined via LPO(p)=1 iff p=0ω, and lim((pi)i∈N)=limi→∞pi. They are related by LPO≡Wlim. The importance of lim is found partially in the
observation from [4] that lim is complete for Baire
class 1 functions, and more generally, that lim(n) is complete
for Baire class n+1 functions.
3 UCNN and CNN
The two Weihrauch degrees of central importance for this paper are unique closed choice and closed choice (on Baire space). These are defined as follows:
Definition 3.1**.**
Given a represented space X, let CX:⊆A(X)⇉X be defined via x∈CX(A) iff x∈A (thus, A∈dom(CX) iff A=∅). Let UCX be the restriction of CX to singletons.
In particular, UCX is capable of finding an element of a given Π10 singleton in X.
In [40] Pauly introduced the notion of iterating a Weihrauch degree f over a given countable ordinal, this is denoted by f†. It is then shown that:
One can read the above result as a very uniform version of the famous
classical result that the Turing downward closures of Π10 singletons in
NN exhausts the hyperarithmetical hierarchy (cf. [42, Corollary
II.4.3]).
Remark:
Seeing that ATR0 asserts the existence of Turing jumps iterated along some countable ordinal and since lim is equivalent to the Turing jump, it may seem as if this theorem already establishes that UCNN is the Weihrauch degree corresponding to ATR0. There is a significant difference here though in what is meant by countable ordinal: In lim†, the input includes a code for something which is an ordinal in the surrounding meta-theory. In particular, any computable ordinal can be used for free. For ATR0 the notion of countable ordinal is that of the model used. For example, an ill-founded computable linear order without hyperarithmetical descending chains (Kleene, see [42, Chapter 3, Lemma 2.1]) counts as an ordinal in the ω-model HYP consisting exactly of hyperarithmetical sets, and a similar phenomenon may happen in non-β-models of ATR0. Things get worse if non-ω-models are considered: ATR0 (indeed, any sound c.e. theory, of course) fails to prove well-foundedness of some computable ordinals.
Note that lim† roughly corresponds to a (uniform)
hyperarithmetical reduction, and therefore Theorem 3.2,
for instance, implies the following:
Corollary 3.3**.**
Whenever {a}∈A(NN) is
computable, then a∈NN is hyperarithmetical.
Corollary 3.4**.**
If f≤WUCNN for f:⊆NN⇉X, then for
every x∈dom(f), f(x) contains some y hyperarithmetical relative to
x.
Corollary 3.3 is a well-known classical fact saying that
every Π10 singleton is hyperarithmetical. Indeed, Spector showed that
every Σ11 singleton is hyperarithmetical (cf. [42, Theorem
I.1.6]). Thus, it is natural to ask whether choice from Σ11
singletons has exactly the same strength as UCNN.
One can generalize Definition 3.1 to any
Γ∈{Σki,Πki,Δki} in a straightforward
manner: Let Γ\mbox−CX:⊆Γ(X)⇉X be defined via x∈Γ\mbox−CX(A) iff x∈A. In other words, any
realizer of Γ\mbox−CX sends a code of a
Γ-definition of A to a name of an element of A. Let
Γ\mbox−UCX be the restriction of
Γ\mbox−CX to singletons. For instance, a
realizer for Σ11-unique choice Σ11-UCNN:⊆Σ11(NN)→NN is a
partial function which, given a Σ11-code of a singleton {x}⊆NN, returns a name of its unique element x. We will see below (in
Theorem 3.11) that Σ11-UCNN≡WUCNN.
There exists computable non-empty A∈A(NN) containing no
hyperarithmetical point.
That is, there is a nonempty Π10 set A⊆NN with no
hyperarithmetical element. This shows that CNN has a computable
instance with no hyperarithmetical solution. Let NHA:NN⇉NN be defined via q∈NHA(p) iff q is not hyperarithmetical
relative to p.
Corollary 3.6**.**
NHA≰WUCNN but NHA≤WCNN.
We now get the separation between UCNN and CNN.
Corollary 3.7**.**
UCNN<WCNN.
There are a number of variants of unique choice, comprehension and separation
that are all equivalent to UCNN w.r.t. Weihrauch reducibility. We
explore some of these next:
Definition 3.8** (Σ11-Separation).**
Let Σ11-Sep:⊆(Tr×Tr)N⇉2N be the multivalued
function with dom(Σ11-Sep)={(Sn,Tn)n∈N:∀n([Sn]=∅∨[Tn]=∅)} that maps any sequence
(Sn,Tn)n∈N in the domain to the set
[TABLE]
One can introduce a similar multivalued function by directly using the space
Σ11(N)×Σ11(N) instead of (Tr×Tr)N without affecting
the Weihrauch degree.
Definition 3.9** (Δ11-Comprehension).**
Let Δ11-CA:⊆(Tr×Tr)N→2N be the restriction of
Σ11-Sep to the set {(Sn,Tn)n∈N:∀n([Sn]=∅↔[Tn]=∅)}. Let Δ11-CA− be the
restriction of Δ11-CA to the set {(Sn,Tn)n∈N:∀n∣[Sn]∣+∣[Tn]∣=1}.
Definition 3.10** (Weak Σ11-Comprehension).**
Let Σ11-CA−:⊆TrN→2N be the function with domain
dom(Σ11-CA−)={(Tn)n∈N:∀n∣[Tn]∣≤1} and that maps
(Tn)n∈N to the unique f∈2N such that f(n)=1↔∣[Tn]∣=1 for all n∈N.
Theorem 3.11**.**
The following are strongly Weihrauch equivalent:
UCNN
2. 2.
Σ11-UCNN
3. 3.
Σ11-Sep
4. 4.
Δ11-CA
5. 5.
Δ11-CA−
6. 6.
Σ11-CA−
Proof.
(Σ11-UCNN≤sWUCNN)
The proof of [40, Theorem
80] implicitly contains a proof ofΣ11-UCN≤sWlim† (in the last
paragraph). It is clear that Σ11-UCNN≡sWΣ11-UCN and that UCNN≡sWUCNN, so the claim follows with Theorem
3.2.
An alternative proof can be obtained by noting that the proof of
UCNN≤sWΔ11-CA− given below is readily adapted to show that
Σ11-UCNN≤sWΔ11-CA instead, and use the reductions below.
(UCNN≤sWΣ11-UCNN)
Trivial, as
id:Π10(NN)→Σ11(NN) is computable by Proposition
2.3(4).
(Σ11-Sep≤sWUCNN)
By [40, Proposition 62 &
Lemma 79]. An alternative proof can be obtained by
combining Lemmata 5.6 and 5.7 below.
(Δ11-CA≤sWΣ11-Sep)
The former is a restriction of the latter.
(Δ11-CA−≤sWΔ11-CA)
The former is a restriction of the latter.
(UCNN≤sWΔ11-CA−)
Let {f} be a singleton of
NN given via some tree T such that [T]={f}. From T we
compute the double-sequence of trees (Tt0,Tt1)t∈N<N
such that: for all t∈N<N,
•
Tt0={s∈T:t⊑s∨s⊑t},
•
Tt1={s∈T:t⊑s}.
Note that, for all t∈N<N, exactly one between Tt0 and Tt1 is ill-founded. In fact, if t⊑f then f∈[Tt0] and, since T has only one path, Tt1 is well-founded. Otherwise, if t⊑f then f∈[Tt1] and [Tt0]=∅. Hence, we even have that for all t∈N<N, ∣[Tt0]∣+∣[Tt1]∣=1.
Since we can identify N<N with N we can consider
g=Δ11-CA−((Tt0,Tt1)t∈N<N). For all t∈N<N, g(t)=0⟺[Tt0]=∅⟺t⊑f. Therefore, given n∈N,
to compute f(n) it suffices to wait for the first t∈Nn+1 such
that g(t)=0 and then put f(n)=t(n). This concludes the proof.
(Δ11-CA−≤sWΣ11-CA−)
For every (Tn0,Tn1)n∈N∈dom(Δ11-CA−) we have that Δ11-CA−((Tn0,Tn1)n∈N)=Σ11-CA−((Tn1)n∈N).
(Σ11-CA−≤sWΣ11-UCNN)
Let
(Tn)n∈N be a sequence of trees in dom(Σ11-CA−). We claim
that using Σ11-UCNN we are able to compute
f∈2N such that:
Finally, since the operations of finite and countable intersection of
Σ11 sets are computable, we are able to uniformly compute from
(Tn)n∈N a name (by Proposition 2.3(2)) for the
Σ11(NN) singleton
[TABLE]
Clearly, applying Σ11-UCNN to such set we obtain the unique f satisfying
(1), which is exactly Σ11-CA−((Tn)n).∎
Arithmetical transfinite recursion
As mentioned above, the operation lim† from
[40] is the ordinal-iteration of the map lim. Here,
we will explore a direct encoding of arithmetical transfinite recursion as a
Weihrauch degree, and give another proof of its equivalence with UCNN.
Let us fix an effective enumeration ⟨ϕn:n∈N⟩ of all
the computable functions ϕ:⊆NN→NN. Note that
LPO(k) is a complete Σk+20-computable function,
and thus one can think of θnk=LPO(k)∘ϕn as the
nthΣk+20-computable function. Instead, we could have used
the nthΣk+20 formula to define an equivalent notion.
Let ATR:⊆2N×WO×N2→2N be the function which maps each (Z,X,(k,n))∈2N×WO×N2 to the set Y∈2N such that, for all (y,j)∈N2,
[TABLE]
where Yj={⟨y,i⟩∈Y:i<Xj}.
Compare Definition 3.12 with ATR0 in reverse mathematics,
cf. [43, Definition V.2.4]. Note that our ATR is
a single-valued function since, as mentioned in the first remark in
this section, our X is truly well ordered, and therefore, we do not need to
consider pseudo-hierarchies.
The following is an analog of the classical reverse mathematical fact
[43, Theorem V.5.1].
Lemma 3.14**.**
ATR≤sWΣ11-Sep.
Proof.
It is easy to see that Σ11-Sep is a cylinder and hence it suffices to show
ATR≤WΣ11-Sep. Given (Z,X,⟨k,n⟩)∈2N×WO×N2, we want to compute
ATR(Z,X,⟨k,n⟩) as defined in Definition
3.12. For each j∈X and Y∈2N, let us consider the
following formula:
[TABLE]
Essentially, H(Y,j) says that Y is the set {⟨y,i⟩∈ATR(Z,X,⟨k,n⟩):i<Xj}. Using now H, we define the following two formulas for each j,z∈N:
[TABLE]
Note that, for each j∈X and z∈N we have φ0(j,z)⟺⟨z,j⟩∈ATR(Z,X,⟨k,n⟩).
Using the function F defined in Lemma 2.4 and the closure
properties of Proposition 2.3, we are able to compute two
names for the Σ11(N2)-sets A0 and A1 corresponding to the
formulas φ0 and φ1. Note that in this case the use of F
is required and we cannot appeal to Proposition 2.3(5) because
k is not fixed but is given with the input. It is easy to see that A0
and A1 are disjoint; hence one can ask Σ11\mbox−Sep to give
us f separating A0 from A1, which is clearly a solution of
ATR(Z,X,⟨k,n⟩). Here are the details:
Since the names for A0 and A1 are Π10(NN×N2)-names, it is not difficult to see that we can build a double sequence of trees (T⟨j,z⟩0,T⟨j,z⟩1)j,z∈N such that, for each j∈N and z∈N,
•
⟨j,z⟩∈A0⟺[T⟨j,z⟩0]=∅,
•
⟨j,z⟩∈A1⟺[T⟨j,z⟩1]=∅.
Note that, if j∈/X then for each z∈N,
¬φ0(j,z) and ¬φ1(j,z), which means that
[T⟨j,z⟩0]=[T⟨j,z⟩1]=∅. If
instead j∈X we have, for each z∈N,
φ0(j,z)⟺¬φ1(j,z) which implies [T⟨j,z⟩0]=∅⟺[T⟨j,z⟩1]=∅.
Therefore the double-sequence of trees (T⟨j,z⟩0,T⟨j,z⟩1)j,z∈N belongs to the domain of
Σ11-Sep. So let f∈Σ11-Sep(T⟨j,z⟩0,T⟨j,z⟩1)j,n∈N. Now we have, for each j∈X and z∈N,
f(j,z)=0⟺[T⟨j,z⟩0]=∅⟺φ0(j,z)⟺⟨z,j⟩∈ATR(Z,X,⟨k,n⟩), i.e. we are
able to compute ATR(Z,X,⟨k,n⟩)∈2N using f.
Note that we are using the original input to test whether j∈X.
∎
Lemma 3.15**.**
Δ11-CA≤sWATR.
Proof.
Let (Tn0,Tn1)n∈N∈dom(Δ11-CA), we want to compute f∈2N
such that, for all n∈N, f(n)=0⟺[Tn0]=∅. In order to
apply ATR we have to specify a set parameter Z, a well ordering
X and an arithmetical formula. The role of Z in this case will be played
by (Tn0,Tn1)n∈N. The well ordering X is obtained as ∑n∈N(KB(Tn0)∗KB(Tn1))+1 (which is a well ordering by
Lemma 2.8(1)).
It remains to specify an arithmetical formula φ(y,Yj⊕Z) which describes what to do at each step of the recursion. We read both Yj and Z as coding a sequence of pairs of trees. The idea is to eliminate at each step the leaves of all the trees in the sequence. Thus, φ(y,Yj⊕Z) holds if either Yj=∅ and y codes a vertex with a child in Z, or y codes a vertex with a child in each tree from Yj. This is easily verified to be an arithmetical formula, and hence can be coded as some θnk.333Similar ideas are found in the investigation of the Weihrauch degree of the pruning derivative of a tree in [35].
Finally, consider Y=ATR((Tn0,Tn1)n,X,⟨k,n⟩),
which is the set we obtain after repeating, along the well ordering X, the
procedure of eliminating leaves from the trees Tn0 and Tn1. Now, let
fix n and consider i∈{0,1} such that Tni is well founded. Note
that, in order to eliminate all the tree Tni, the recursion should be
done at least over the ordinal rank(Tni). In our case, the recursion is
done over X whose order type is greater than the order type of KB(Tni) which in turn is greater than rank(Tni), cf. Lemma
2.8(2). This means that Y does not contain any element of the
tree Tni. This argument applies to each well founded tree in the sequence
(Tn0,Tn1)n, so we can know whether a tree in the sequence has a path
or not simply by checking if its root is in Y. It is easy to see that this
allows us to compute Δ11-CA((Tn0,Tn1)n∈N).
∎
4 Σ11-weak König’s lemma
4.1 Σ11 versus Π11
In this section, we focus on the following contrast between reverse
mathematics and the Weihrauch lattice regarding Σ11 and
Π11-separation: On the one hand, in reverse mathematics, we have
[TABLE]
where A<B indicates RCA0⊢B→A,
but RCA0⊬A→B. On the other hand, in the
Weihrauch lattice, we have
[TABLE]
The former inequality (3) was proven by Montalbán
[32] using Steel’s tagged tree forcing. The latter inequality
(4) follows from the well-known fact in descriptive set
theory that Σ11 has the Δ11-separation property, while Π11 does
not (see also Lemma 4.4). It is not hard to explain the cause
of the contrast between (3) and
(4), namely the Spector-Gandy phenomenon.
Let M be an ω-model, and let (Σ11)M be the
collection of all subsets of ω which are Σ11-definable within
M, that is,
(Σ11)M={{n∈ω:M⊨φ(n)}:φ∈Σ11}.
We define (Π11)M analogously. Consider the ω-model HYP consisting of all hyperarithmetical reals. The Spector-Gandy theorem
(cf. [42, Theorem III.3.5 + Lemma III.3.1] or [43, Theorems
VIII.3.20 + VIII.3.27]) implies that
[TABLE]
The roles of Σ11 and Π11 are interchanged! We should always be
careful about this role-exchange phenomenon of Σ11 and Π11 when
comparing reverse math and computability theory. Of course, the notion of a
β-model solves this role-exchange problem. To be precise, a β-model (see [43, Section VII]) is an ω-model
M satisfying the following condition:
[TABLE]
However, the notion of a β-model is obviously related to closed choice
CNN: An ω-model M is a β-model iff, for any
Z∈M and non-empty Π10(Z) set P⊆NN, some
α∈P belongs to M. Therefore, when studying principles
weaker than CNN, we cannot work within the β-models.
Now, how should we interpret the reverse-mathematical Σ11-separation
principle in our real universe? The right answer may not exist. It may
be Π11-Sep or may be Σ11-Sep.
We have already examined the strength of the Σ11-separation principle
Σ11-Sep. In this section, we will investigate the Π11-separation
principle, Π11-Sep, in the Weihrauch lattice. In reverse mathematics,
Montalbán [32] showed that the strength of the Π11-separation
principle is strictly between Δ11\mbox−CA0 and ATR0
(444Actually, Montalbán showed that Π11-separation is strictly
weaker than Σ11\mbox−AC.):
[TABLE]
Moreover, Δ11\mbox−CA0 and Π11\mbox−SEP0 are theories of hyperarithmetic analysis, that is, for every Z⊆ω,
HYP(Z) is the least ω-model of that theory containing Z. On
the other hand, HYP⊨ATR0. In contrast, we will see
the following:
[TABLE]
4.2 The strength of Σ11-weak König’s lemma
The principle of Π10-separation was studied already in the precursor
works by Weihrauch [45], and Weak König’s Lemma (aka closed
choice on Cantor space) was a focus in the earliest work on Weihrauch
reducibility in the modern understanding
[21, 8, 6]. Here, we explore their higher-level
analogues.
Let Π11-Sep be the following partial multivalued function: Given
Π11-codes of sets A,B⊆N, if A and B are disjoint, then
return a set C⊆N separating A from B, that is, A⊆C
and B∩C=∅. To be more precise:
Definition 4.1**.**
Let Π11-Sep:⊆Π11(N)×Π11(N)⇉2N be
such that C∈Π11-Sep(A,B) iff C separates A from B, where
(A,B)∈dom(Π11-Sep) iff A∩B=∅.
We also consider Σ11-weak König’s lemma Σ11-WKL: Given a Σ11-code
of a set T⊆2<ω, if T is an infinite binary tree, then
return a path through T. Formally speaking:
Definition 4.2**.**
Let Σ11-WKL:⊆Σ11(2<ω)⇉2N be such that
p∈Σ11-WKL(T) iff p is an infinite path through T, where T∈dom(Σ11-WKL) iff T is an infinite binary tree.
While Σ11-WKL appears as a Σ11-version of closed choice on Cantor space,
it is not equivalent to Σ11-choice on 2N (nor, equivalently, closed
choice on NN). Instead, it is equivalent to the parallelization
Σ11\mbox−C2 of Σ11 choice on the discrete
space 2={0,1}. We will show the following.
We will use the following fundamental notion in HYP-theory.
A Π11-norm on a Π11 set P⊆N is a map φ:N→ω1CK∪{∞} such that P={n:φ(n)<∞} and that the following relations ≤φ and <φ are Π11:
[TABLE]
It is well-known that every Π11 set admits a Π11-norm (in an
effective manner): Consider a many-one reduction from a Π11 set P to
the set WO of well orderings. We will explore the uniform complexity
of this kind of stage comparison principle in Section 5.
One can easily separate unique choice on NN and the Π11-separation
principle by considering the diagonally non-hyperarithmetical
functions, which is a HYP version of DNC2 (known as diagonally
noncomputable functions). A very basic fact in HYP-theory is the existence of
a computable enumeration (ψe)e∈N of all partial Π11
functions on N. For instance, let ψe be a standard
Π11-uniformization of the ethΠ11 set
Pe⊆N×N, that is, ψe(n) is an element in the nth
section of Pe attaining the smallest φ-value if it exists, where
φ is a Π11-norm on Pe.
Lemma 4.4**.**
UCNN<WΠ11-Sep.
Proof.
To see that UCNN≤WΠ11-Sep, note that UCNN≡WΔ11-CA by
Theorem 3.11, and Δ11-CA≤WΠ11-Sep is
straightforward. For the separation, let (ψe)e∈N be an
enumeration of all partial Π11 functions on N as above. For i<2,
consider Pi={e∈N:ψe(e)↓=i}. Clearly Pi is Π11,
and P0∩P1=∅. It is easy to see that there is no Δ11
set separating P0 and P1.
∎
The proof of Lemma 4.4 motivates us to introduce the
following multivalued function Π11\mbox−DNC2:2N⇉2N: Given an oracle X, return a two-valued
X-diagonally non-hyperarithmetical function f, that is, f∈Π11\mbox−DNC2(X) iff, whenever ψeX(e)↓, f(e)=ψeX(e), where (ψeX)e∈N is a canonical enumeration of
all partial Π11(X) functions on N. The following is an analog of the
well-known fact that every DNC2-function has a PA-degree.
Proposition 4.5**.**
Π11-Sep≡WΠ11\mbox−DNC2.
Proof.
Let P0 and P1 be disjoint Π11 sets. Clearly there is e such
that n∈Pi iff ψe(n)↓=i. By the recursion theorem, one
can uniformly find a computable function r such that ψr(n)(r(n))≃ψe(n). Let f be a diagonally non-hyperarithmetical function. If
f(r(n))=i then ψr(n)(r(n))≃ψe(n)=i, which implies n∈/Pi. Therefore, S={n:f(r(n))=1} separates P0 from P1. This
argument is easily relativizable uniformly. The converse direction is also
clear.
∎
Using a Π11-norm, one can show Σ11-WKL≡WΠ11-Sep by modifying the
usual proof of the well-known equivalence between WKL and Σ10-Sep.
Lemma 4.6**.**
Σ11-WKL≡WΠ11-Sep≡WΣ11\mbox−C2.
Proof.
By a straightforward modification of the usual proof of Σ10-Sep≡WC2, it is easy to see that Π11-Sep≡WΣ11\mbox−C2 holds. It is also clear that
Π11-Sep≤WΣ11-WKL. Thus, it suffices to show that Σ11-WKL≤WΠ11-Sep.
Given a Σ11-tree T⊆2<ω, let ExtT⊆2<ω be the set of all extendible nodes of T. Clearly, its complement
¬ExtT=2<ω∖ExtT is Π11, and thus
admits a Π11-norm φ (we need to get φ in a uniform way,
but it is straightforward). Consider the Π11 set Pi={σ:σ\mbox⌢i<φσ\mbox⌢(1−i)} for each i<2. Obviously, P0∩P1=∅. We claim that
[TABLE]
If σ∈/Pj then σ\mbox⌢j<φσ\mbox⌢(1−j), that is,
either φ(σ\mbox⌢j)=∞ or φ(σ\mbox⌢(1−j))≤φ(σ\mbox⌢j) holds. If the former holds then we must have σ\mbox⌢j∈ExtT. If φ(σ\mbox⌢j)<∞, then we must have
φ(σ\mbox⌢(1−j))=∞ since σ∈ExtT implies that
σ\mbox⌢i∈ExtT for some i<2. By the latter condition,
∞=φ(σ\mbox⌢(1−j))≤φ(σ\mbox⌢j); hence
φ(σ\mbox⌢j) must be ∞. In any case, we have
φ(σ\mbox⌢j)=∞, which means that σ\mbox⌢j∈ExtT.
This verifies the above claim.
Let S be such that P0⊆S and S∩P1=∅. Let
σ0 be the empty string, and put σn+1=σn\mbox⌢S(σn). Then, by the above claim, we have σn∈ExtT for
any n, and therefore ⋃nσn∈[T]. One can easily relativize
this argument uniformly.
∎
Lemma 4.7**.**
Σ11-WKL<WΣ11\mbox−CN.
Proof.
By Lemma 4.6, we have Σ11-WKL≤WΣ11\mbox−CN. It remains to show that
Σ11\mbox−CN≰WΣ11-WKL. It is easy to see that Σ11-WKL
is a cylinder, and hence it suffices to show that
Σ11\mbox−CN≰sWΣ11-WKL.
We first show the following claim: Let T⊆2<ω be a
Σ11 tree, and Φ a Turing functional such that for every x∈[T], Φx is total. Then there exists a Δ11 function h:N→N majorizing n↦Φx(n) for every x∈[T].
Let g:N→N be a function such that for any n, if ∣σ∣=g(n) then
either σ∈/ExtT or Φσ(n)↓. This
condition is clearly Π11, and by compactness, g is total. Hence, g
is a total Π11 function, and thus actually Δ11. Then define
h(n)=max{Φσ(n):∣σ∣=g(n)\mboxandΦσ(n)↓}. Clearly h is Δ11 and Φx(n)≤h(n) for any x∈[T]. This verifies the claim.
Let (ψe)e∈ω be a computable enumeration of partial Π11 functions on N.
Let Se be the set of all k such that
[TABLE]
Clearly Se is Σ11 and cofinite. Then every element of
S=∏eSe dominates all Δ11 functions. If
Σ11\mbox−CN≤sWΣ11-WKL then we must have a
Σ11-tree T⊆2<ω whose paths compute uniformly an
element of S, which is impossible by the above claim.
∎
Recall that A⋆B denotes the sequential composition of A and B,
cf. [16], that is, a function attaining the greatest
Weihrauch degree among {g∘f:g≤WA\mboxandf≤WB}.
Proposition 4.8**.**
Σ11-WKL⋆Σ11-WKL≡WΣ11-WKL.
Proof.
This is a modification of the independent choice theorem from
[6]. We can assume that the inputs to Σ11-WKL⋆Σ11-WKL are
a computable function f, z∈2N as well as (relativizable)
Σ11 trees S and T. Then, {x⊕y:x∈[Sz]\mboxandy∈[Tf(z,x)]} is a Σ11 closed set, and any of its elements is a
solution to Σ11-WKL⋆Σ11-WKL.
∎
There is a natural principle between UCNN and Σ11-WKL. Let us define
Σ11-weak weak König’s lemma Σ11\mbox−WWKL as follows: Given
a Σ11 set T⊆2<ω, if T is an infinite binary tree and if
[T] has a positive measure, then return a path through T. This is in
analogy to the usual weak weak König’s lemma, whose Weihrauch degree was
studied in [15, 9, 11].
Note that Hjorth and Nies (see [34, Chapter 9.2]) showed that there
is a Σ11-closed set consisting of Π11-Martin-Löf random
reals. Indeed, the proof shows that Π11\mbox−MLR is Weihrauch
reducible to Σ11\mbox−WWKL, where Π11\mbox−MLR is a
multivalued functions representing Π11-Martin-Löf randomness, which
is introduced in a straightforward manner. We also have WKL≰WΣ11\mbox−WWKL since the Turing upward closure of any nontrivial
separating class has measure zero (cf. [26, Theorem 5.3]). We show
that, even if we enhance Σ11\mbox−WWKL by adding a
hyperarithmetical power, its strength is strictly weaker than Σ11-WKL:
Theorem 4.9**.**
UCNN<WUCNN⋆Σ11\mbox−WWKL<WΣ11-WKL.
Proof.
The inequality UCNN<WUCNN⋆Σ11\mbox−WWKL is
obvious since no Π11-Martin-Löf random real is hyperarithmetic.
Moreover, by Proposition 4.8, we have UCNN⋆Σ11\mbox−WWKL≤WΣ11-WKL. Suppose for the sake of
contradiction that Σ11-WKL≤WUCNN⋆Σ11\mbox−WWKL.
Then, for any Σ11 closed set S, there are a Σ11 closed
set P of positive measure and a Π11 function f:P→S, so that
f(x)≤hx for any x∈P.
In particular, assume that S is the set of all Π11\mbox−DNC2
functions, and let P and f be as above. It is known that x is
Π11-random iff x is Δ11-random and ω1CK,x=ω1CK (see [34, Theorem 9.3.9]). Since there are
conull many Π11-random reals, Q={x∈P:ω1CK,x=ω1CK} also has positive measure. Given x∈Q, there is an ordinal
α<ω1CK,x=ω1CK such that f(x)≤Tx⊕∅(α) (cf. [17, Lemma 4.2] and
[2, Section 2.3.2]). As in [26, Theorem 5.3], it is easy to
see that the ∅(α)-Turing upward closure,
{S}_{\alpha}=\{z:h\leq_{T}z\oplus\emptyset^{(\alpha)}\mbox{ for some h\in S}\}, of S has measure zero for any computable ordinal α. Hence,
S^=⋃{Sα:α<ω1CK} is also null. Our
previous argument shows that Q⊆S^, however μ(S^)=0
contradicts μ(Q)>0.
∎
Two statements which are equivalent to ATR0 in the context of
reverse mathematics are comparability of well orderings and weak
comparability of well orderings ([43, Theorem V.6.8] and
[20]). These involve two kinds of effective witnesses that
one well ordering is shorter than another: strong comparison maps and order
preserving maps.
Definition 5.1**.**
If X,Y∈WO then we say that f:N→N is a strong comparison
map between X and Y, in symbols f:X≤sY, if the following
conditions hold:
•
∀n(n∈/X→f(n)=0),
•
∀n,m∈X(n≤Xm↔f(n)≤Yf(m)),
•
∀n∈X∀k∈Y(k≤Yf(n)→∃m∈Xf(m)=k).
In other words, f is an order embedding of X into Y whose image is an initial segment of Y.
Definition 5.2** (Comparability of well orderings).**
Let CWO:WO×WO→NN be the function that maps any pair
(X,Y) of countable well orderings to the unique f∈NN such that
f:X≤sY or f:Y+1≤sX.
The use of Y+1 in the previous definition makes sure that f is unique
even when X and Y are isomorphic.
Definition 5.3**.**
If X,Y∈LO we say that f:N→N is an order preserving map between X and Y, in symbols f:X≤Y, if the following conditions hold:
•
∀n(n∈/X→f(n)=0),
•
∀n,m∈X(n≤Xm↔f(n)≤Yf(m)),
Definition 5.4** (Weak comparability of well orderings).**
Let WCWO:WO×WO⇉NN be the multivalued function
that maps any pair (X,Y) of countable well orderings to the set
{f∈NN:(f:X≤Y)∨(f:Y≤X)}.
The following classifies the Weihrauch degree of comparability of well
orderings:
If X,Y∈WO, the conjunction of the three conditions in Definition
5.1 is a Π20 formula with X,Y and f as free variables. In
particular, a name for the Π20 set {f}=CWO(X,Y) is computable from
X and Y. Then, since UCNN≡sWΠ20\mbox−UCNN by Theorem
3.11 and Proposition 2.3, we can use the
second one to obtain f.
∎
Lemma 5.7**.**
Σ11-Sep≤sWCWO.
Proof.
We follow essentially the proof of Theorem V.6.8 in [43]. The
only modification concerns the definition of the well orderings U and V,
for which the original proof uses the Σ11 bounding principle.
So, let (Sn,Tn)n∈ω be a double-sequence of trees in
dom(Σ11-Sep). Without loss of generality we assume that for all n∈N,
Sn and Tn are non-empty. We can build the corresponding double-sequence
of linear orderings (Xn,Yn)n such that, for all n, Xn=KB(Sn) and Yn=KB(Tn). Note that, since
(Sn,Tn)n∈dom(Σ11-Sep), we have
[TABLE]
Consider U=∑n∈N(Q∗Yn)∗Xn, which by (5) and by
Lemma 2.8.1 is a well ordering. We claim that the following holds:
[TABLE]
In fact, let X∈LO and n be such that ¬WO(Xn). Then by
(5) we have WO(Yn), which means that X∗Yn is also a
well ordering. Furthermore, by 3 and 2 of Lemma 2.8, we have
∣X∗Yn∣≤∣Q∗Yn∣≤∣(Q∗Yn)∗Xn∣<∣U∣.
For all n∈N, define Zn=(U+Xn)∗Yn. By (6) and by 1
and 2 of Lemma 2.8 we have, for all n∈N,
[TABLE]
Finally, consider V=U+∑n∈NZn and define the well orderings
•
Z=∑n∈N(Zn+V⋅N),
•
W=∑n∈N(V+V⋅N).
Note that all the well orderings we defined so far, in particular Z and
W, are computable from the double-sequence (Xn,Yn)n. In the
construction of V we can also use a special mark for its least element.
Furthermore, we can code Z in such a way that, if x∈Zn+V⋅N, for
some n∈N, then we are able to compute whether x belongs to Zn or to
the first copy of V, and in the second case, whether x belongs to the
copy of U contained in V. Similar assumptions can be made for the
construction of W.
Let now f=CWO(Z,W) be the comparing map between Z and W. Since
∣Zn+V⋅N∣=∣V+V⋅N∣ for all n, we have ∣Z∣=∣W∣ and f is the
isomorphism of Z onto W. In particular, for each n∈N, f induces an
isomorphism fn of Zn+V⋅N onto V+V⋅N. Define g∈2N by
g(n)=0 if and only if the image of Zn under fn is a strict initial
segment of U, i.e. ∣Zn∣<∣U∣. This can be done computably by checking
whether fn maps the first element of the first copy of V in
Zn+V⋅N to U or not. Then, recalling the definition of
(Xn,Yn)n, if [Sn]=∅ then ¬WO(Xn) and, by
(7), ∣Zn∣<∣U∣ so that g(n)=0. Similarly, if
[Tn]=∅ then, by (8), ∣U∣≤∣Zn∣ so that
g(n)=1.
∎
The Weihrauch degree of weak comparability of well orderings, however, has
eluded our classification attempts:
Question 5.8**.**
Does WCWO≡WUCNN?
Recently, Jun Le Goh [22] obtained a positive answer to our question.
6 The one-sided versions of PTT and open determinacy
Both the perfect tree theorem and open determinacy have at its core a
disjunction A∨B which is not to be read constructively. A
typical approach to formulate these as computational tasks is to view these
as implications ¬A⇒B or ¬B⇒A. In this
section, we explore these variants.
Recall that a tree is perfect if every node has at least two incomparable
extensions. In particular, every perfect tree is pruned. The perfect tree
theorem states that every tree with uncountably many paths has a perfect
subtree and leads to the following two problems: The first problem is given a
closed set A which has no perfect subset (that simply means that A is
countable), and has to show its countability, that is, to enumerate all
elements of A. We consider two variants of this task, depending on what
exactly is meant by listing. The weak version contains no information
about the cardinality, the strong version does. The second problem is more
direct: it asks to find a perfect subset of a given tree with uncountably
many paths.
Definition 6.1**.**
wList:⊆A(NN)⇉(NN)ω maps a countable
set A to some ⟨b0p0,b1p1,…⟩ such that A={pi∣bi=1}. List:⊆A(NN)⇉(NN)ω
maps a countable set A to some n⟨p0,p1,…⟩ such that
either n=0, pi=pj for i=j and A={pi∣i∈N}; or n>0, ∣A∣=n−1 and A={pi∣i<n−1}.
Definition 6.2**.**
PTT1:⊆Tr⇉Tr maps T such that [T] is uncountable to
some perfect T′⊆T.
We start by reporting a result originating from discussion during the
Dagstuhl seminar on Weihrauch reducibility [14], in
particular including a contribution by Brattka:
Proposition 6.3**.**
PTT1≡WCNN.
Proof.
For CNN≤WPTT1, note that from A∈A(NN) we can
compute a tree T such that [T]=A×NN. If A is non-empty,
then [T] is uncountable. Given some perfect subtree T′ of T, we can
compute a path through T′ and hence through T. By projecting, we obtain a
point in A.
For PTT1≤WCNN, call a function λ:N<N→N a
modulus of perfectness for T, if v∈T implies that there are
incomparable u,w∈[0,λ(v)]λ(v) with vu,vw∈T. A
non-empty tree has a modulus of perfectness iff it is perfect, and given T
the set
[TABLE]
is closed, and non-empty for [T] uncountable by
the perfect tree theorem. Taking into account that Tr×N(N<N) is computably isomorphic to NN, we can thus apply
CNN and project to obtain a perfect subtree of T.
∎
6.1 Listing the points in a countable set
We now examine the strength of the contrapositive of the perfect tree theorem
PTT1, which is List in our setting as explained above.
Theorem 6.4**.**
wList≡WList≡WUCNN.
The main ingredient of our proof is a variant of the Cantor-Bendixson
decomposition, designed in such a way that it can be carried out in a Borel
way. This modified version works as the usual one for countable sets, but can
differ for uncountable ones555Kreisel has shown that computable A∈A(NN) may have uncomputable Cantor-Bendixson rank
[30]. As any total function from NN into the countable ordinals
that is effectively Borel is dominated by a computable function (the Spector
Σ11-boundedness principle, cf. [40]), this implies
that the Cantor-Bendixson decomposition cannot be done in a Borel way.. If
u and w are finite words on N, u⊑w means that u is a
prefix of w.
Definition 6.5**.**
A one-step mCB-certificate of A∈A(NN) consists of
(a)
A prefix-independent666Meaning that wi⊏wj never
holds. sequence (wi)i∈N of finite words ordered in a
canonical way,
2. (b)
A sequence of bits (bi)i∈N which are not all [math],
3. (c)
A sequence of points (pi)i∈N
subject to the following constraints:
If bi=1, then pi∈A∩wiNN.
2. 2.
If bi=0, then ∀p∈HYP(A)p∈/A∩wiNN and pi=0ω.
3. 3.
∀p,q∈HYP(A)(p∈A∩wiNN∧q∈A∩wiNN⇒p=q).
4. 4.
If wi⊑w for all i∈N, then ∃p,q∈A∩wNNp=q.
For a one-step mCB-certificate for A, its residue is A∖⋃i∈NwiNN.
Definition 6.6**.**
A global mCB-certificate for A∈A(NN) is indexed by
some initial I⊆N (which may be empty). It consists of a sequence
(ci)i∈I of one-step mCB-certificates such that there exists a
linear ordering ⊏⊆I×I with minimum [math]
(if non-empty), such that c0 is a one-step mCB-certificate for A, for
each n∈I∖{0}, cn is an mCB-certificate for ⋂i⊏nAi, where Ai is the residue of ci; and ∀p∈HYP(A)p∈/A∩⋂i∈IAi.
Lemma 6.7**.**
The set of global mCB-certificates of A is uniformly Σ11 in A.
Proof.
This is almost immediate from the definition, besides the quantification over HYP. That this is unproblematic follows from Kleene’s HYP-quantification theorem [28, 29] (the converse of the Spector-Gandy theorem).
∎
Lemma 6.8**.**
For non-empty non-perfect A∈A(NN), A has a one-step
mCB-certificate such that its residue is equal to its Cantor-Bendixson
derivative. If all points in A are hyperarithmetical relative to A, then
A has a unique one-step mCB-certificate.
Proof.
Let (qj) be the finite or infinite list of isolated points in A, and let
(uj) be the shortest prefix such that A∩ujNN={qj}. It
follows from Corollary 3.3 applied to A∩ujNN
that each qj is hyperarithmetical relative to A. Let (vk) be the list
of shortest prefixes such that A∩vkNN=∅, excluding those
extending some uj. Now the sequence (wi) is obtained such that {wi}={uj}∪{vk}, subject to the canonical ordering condition. If wi=vk, then bi=0 and pi=0ω, if wi=uj then bi=1
and pi=qj.
It is immediate that the construction satisfies Conditions (1,2,3,4) and that
the residue sees exactly the isolated points removed, i.e. is the
Cantor-Bendixson derivative of A. It remains to argue that the
mCB-certificate constructed as such is unique if all points in A are
hyperarithmetical relative to A (this is a classic result, of course). As
the choice of bi and pi was uniquely determined by the sequence
(wi), we only need to prove that there is no alternative sequence
(wi′). As no wi can satisfy the conclusion of Condition (4), we know
that for each wi there exists some wi′′ with wi′′⊑wi.
Assume that wi′′⊏wi for some i. If bi=1, then wi
was chosen minimal under the constraint that A∩wiNN is a singleton,
A∩wi′′ contains at least two points, which are both
hyperarithmetical. Hence, wi′′ fails Condition (3). If bi=0, then
wi′′NN∩A=∅ contradicts the choice of vk as shortest
prefix, ∣wi′′NN∩A∣=1 contradicts the choice of uj as
shortest prefix of an isolated point in A, and ∣wi′′NN∩A∣≥2 again violates Condition (3). Hence we know that all (wi) must appear
as some (wi′′).
Assume that there is some w occurring as a wi′′ but not as a wi. As
the (wi′′) are prefix-free, w is not an extension of some wi.
Hence, Condition (4) for the (wi) implies that ∣A∩wNN∣≥2.
But as all points in A are hyperarithmetical, this shows that neither the
conclusion of Condition (2) nor that of Condition (3) can be satisfied for
wi′′=w, and we have obtained the desired contradiction.
∎
Corollary 6.9**.**
If A∈A(NN) is countable, then A has a
unique global mCB-certificate, the pi for bi=1 occurring in some
one-step mCB-certificate list all points in A, and the order type of the
implied linear ordering is the Cantor-Bendixson rank of A plus 1.
That UCNN≤WwList is simple: Any instance of the former is an
instance of the latter, and from a list repeating a single element, we can
recover that element. For the other direction, we show wList≤WΣ11-UCNN
instead and invoke Theorem 3.11. By Lemma
6.7 the set of global mCB-certificates of A∈A(NN) is computable as a Σ11-set from A, and by
Corollary 6.9 this is a singleton for countable A. We can
distinguish whether the global mCB-certificate uses an empty or non-empty
linear order. In the former case, the set is empty, and in the latter case,
we can compute a list of all points in A.
Again, wList≤WList is trivial. For the reverse direction, we observe
that List≤WUCNN⋆wList, since UCNN more than suffices
to extract the required additional information from an unstructured list. We
then use the preceding result and UCNN≡WUCNN⋆UCNN
from [6].
∎
Regarding the non-uniform aspect, it is known that every countable Π10
(indeed Σ11) set A⊆NN consists only of hyperarithmetical
elements ([42, Theorem III.6.2]). Theorem 6.4 concludes
that every countable Π10 set A⊆NN admits a
hyperarithmetical enumeration. Combining Proposition 6.3 (and
Gandy’s basis theorem [42, Corollary III.1.5]) and Theorem
6.4, we indeed get the following:
Corollary 6.10**.**
For any computable tree T⊆ω<ω, either T has a hyperlow
perfect subtree or there is a hyperarithmetical enumeration of all infinite
paths through T.
Listing on Cantor space
We have seen that for subsets of Baire space, it makes no difference whether
we intend to list all points of a countable set or all points of a finite
set. We briefly explore the corresponding versions for Cantor space. Let
List2N,<ω:⊆A(2N)⇉(2N)∗ denote the
problem to produce a tuple of all elements of a finite closed subset of
2N (i.e. (p0,…,pn−1)∈List2N,<ω(A) iff A={pi∣i<n}). Let wList2N,≤ω:⊆A(2N)⇉(2N)ω denote the problem to list all elements
of a non-empty countable closed subset of 2N (i.e. (pi)i∈N∈wList2N,≤ω(A) iff {pi∣i∈N}=A). Note that List2N,<ω is not a restriction of
wList2N,≤ω, since finite tuples and lists with finite range
have distinct properties. We will in fact show in Corollary 6.15
that these two multivalued functions are incomparable with respect to
Weihrauch reducibility.
Proposition 6.11**.**
List2N,<ω≡WΠ20\mbox−CN.
Proof.
To see that List2N,<ω≤WΠ20\mbox−CN, note that we can
guess a finite partition of 2N into clopens A0,…,An such that
∣A∩Ai∣=1 for input A and any i. Verifying a correct partition
is Π20 (because A∩Ai=∅ and ∣A∩Ai∣≤1 are
respectively a Π10 and a Π20 condition), and given a correct
partition, we can compute the listing since UC2N is computable.
For the other direction, note that we can view Π20\mbox−CN as the
following task: Given (p0,p1,…)∈(2N)ω with the promise
that if ∣{j∣pi(j)=1}∣=∞ then ∣{j∣pi+1(j)=1}∣=∞, and that there exists some i with ∣{j∣pi(j)=1}∣=∞, find such an i (for details, see [10]). We now
construct A∈2N as follows: For each i, keep track of an auxiliary
variable ki, which is initially [math]. Start enumerating all 0⟨i,k⟩1 into the complement of A except the 0⟨i,ki⟩1. Also enumerate all 0l1s0. Whenever we read another 1 in
pi, we do enumerate 0⟨i,ki⟩1, and set the new ki to
be the least k such that 0⟨i,k⟩1 has not been enumerated
yet.
Whenever ∣{j∣pi(j)=1}∣<∞ for some i, then ki will eventually remain constant. The resulting set A will be of the form {0ω}∪{0⟨i,ki⟩1ω∣i∈I} where I is the finite set of non-solutions. Having a finite listing of A lets us easily pick some solution.
∎
As a corollary one can see that every finite Π10 subset of 2N
admits a computable listing uniformly in 0′′, and the complexity
0′′ is optimal: If a function f sends an index (i.e. a Gödel
number) of a Π10 set P⊆2N to an index of a computable
listing of elements of P whenever P is finite, then f must compute
0′′.
To note that wList2N,≤ω is parallelizable, observe that we
can effectively join countably many trees along a comb, and the set of paths
of the result is essentially the disjoint union of the original paths. The
second reduction follows from the obvious embedding of 2N into NN as
a closed set and Theorem 6.4. For the third reduction, note that
we can embed NN as a Π20-subspace B into 2N such that 2N∖B is countable. Given some singleton A∈A(NN), we
can compute some countable Aˉ∈A(2N) such that Aˉ∩B is the image of A under that embedding. If we have a list of all
points in Aˉ, we can then use Π20\mbox−CN to pick the one
in B. That the third reduction is an equivalence follows from the second,
the observation that Π20\mbox−CN≤WUCNN and UCNN⋆UCNN≡WUCNN (cf. [6]).
∎
Proposition 6.13**.**
lim≤WwList2N,≤ω.
Proof.
Consider the map id:A(N)→O(N) translating an
enumeration of a complement of a set to an enumeration of the set. Studied
under the name EC in [44], it is known to be equivalent to
lim. Now from A∈A(N) we can compute {0ω}∪{0n1ω∣n∈A}∈A(2N). From any list of
the elements of the latter set, we can then compute A∈O(N).
∎
Proposition 6.14**.**
The following are equivalent for single-valued f:⊆X→NN where X is a represented space:
To see that 2. implies 1., consider some single-valued f:⊆NN→NN with f≤WwList2N,≤ω. So from any p∈dom(f), we can compute some countable Ap∈A(2N), and from
any enumeration of the points in Ap together with p we can compute
f(p) via some computable K. We will argue that having access to a pruned
tree T with [T]=Ap suffices to compute f(p), and note that pruning a
binary tree is equivalent to lim (see
e.g. [35]). Let us assume that there are prefixes w0,…,wn in the pruned tree such that K upon reading p and
w0,…,wn outputs some prefix w. Then there is some enumeration
q0,q1,… of points in Ap such that w0,…,wn are prefixes
of q0,…,qn, hence w is a prefix of f(p). Conversely, for any
fixed enumeration q0,q1,… of points in Ap and desired prefix
length m of f(p) there is some k∈N such that K outputs
f(p)≤m after having read no more than the k-length prefixes of
qi for i≤k. Moreover, each (qi)≤k occurs in the pruned
tree T. Thus, having access to T lets us compute longer and longer
prefixes of f(p), and since f is single-valued, this suffices to compute
f(p).
∎
In particular, A⊆N is computable from all listings of some countable Π10 set P⊆2N iff A is 0′-computable. On the other hand, there is no computable ordinal α such that 0(α) computes a listing of any countable Π10 subset of 2N.
Corollary 6.15**.**
List2N,<ω≰WwList2N,≤ω and
wList2N,≤ω≰WList2N,<ω.
Proof.
For the first claim, it is known that Π20-CN≡WΠ20-UCN
[10]. (Sketch: Take (pi)i∈N as in Proposition
6.11, and then put p^i,s(n)=1 iff pi(n)=1 and
pj(t)=0 for all j<i and s≤t<n. It is easy to see that there is a
unique i,s such that ∣{n∣p^i,s(n)=1}∣=∞, and then
∣{n∣pi(n)=1}∣=∞.) Then observe that Π20-UCN is
single-valued, and that lim is Σ20-computable while
Π20-CN is not. The claim then follows by Proposition 6.14.
The second claim follows from the observation that any solution of a
(computable) instance of Π20-CN must be computable, while lim has computable instances without computable solutions.
∎
In Proposition 6.13 we have shown that lim≤WList2N,≤ω, which implies
Π20\mbox−CN≤Wlim⋆lim≤WwList2N,≤ω⋆wList2N,≤ω; hence the
assertion follows from Proposition 6.12 and UCNN⋆UCNN≡WUCNN. The strictness follows from Proposition
6.14 since UCNN is single-valued and UCNN≰Wlim.
∎
Question 6.17**.**
Does wList2N,≤ω⋆wList2N,≤ω≡WUCNN hold?
The feature that wList2N,≤ω is not closed under composition
itself, but that the hierarchy of more and more compositions stabilizes at a
finite level, seems surprising for a natural degree. A similar
observation was made before regarding the degree of finding Nash equilibria
in bimatrix games [27].
6.2 Finding winning strategies
We now move on to the complexity of finding winning strategies in open
Gale-Stewart games. In formulating the corresponding multivalued functions,
we implicitly code strategies in sequential games into Baire space elements.
Definition 6.18**.**
FindWSΣ:⊆O(NN)⇉NN (FindWSΠ:⊆O(NN)⇉NN) maps an open game where Player 2 (Player 1) has
no winning strategy to a winning strategy for Player 1 (Player 2). Likewise,
FindWSΔ maps a clopen game where Player 2 has no winning strategy to a
winning strategy for Player 1. Here a name for a clopen set consists of two
names for open sets which are one the complement of the other.
On the one hand, the difficulty of finding a winning strategy for a closed
player is the same as the closed choice on Baire space.
Proposition 6.19**.**
FindWSΠ≡WCNN.
Proof.
For CNN≤WFindWSΠ, note that we can turn any A∈A(NN) into a Σ10 game where Player 1’s moves do not matter,
and Player 2 wins iff his moves form a point p∈A.
For FindWSΠ≤WCNN, note that given a Player 2 strategy τ
and the Σ10 winning condition W⊆NN we can compute a tree
TW,τ describing the options available to Player 1: Essentially, the
strategies σ winning against τ correspond to finite paths in
TW,τ ending in a leaf, whereas strategies σ′ losing against
τ correspond to infinite paths through TW,τ. Thus, τ is a
winning strategy for Player 2 iff TW,τ is a pruned tree, i.e. a
tree without any leaves. Let λ:N∗→N be a witness of
prunedness of T iff ∀v∈Tvλ(v)∈T. If Player 2
has a winning strategy for the game W, then the set
[TABLE]
is a non-empty closed set computable from W, and projecting a member of it yields a winning strategy for Player 2.
∎
On the other hand, the difficulty of finding a winning strategy for a open/clopen player is the same as the unique choice on Baire space. In the case of clopen games, we even get full determinacy defined as follows:
Definition 6.20**.**
DetΔ:Δ10(NN)⇉NN×NN maps a clopen game W to a pair
of strategies σ, τ such that either σ is winning for
Player 1 or τ is winning for Player 2 (i.e. a Nash equilibrium).
Theorem 6.21**.**
FindWSΔ≡WDetΔ≡WFindWSΣ≡WUCNN.
We will prove Theorem 6.21 using the following lemmata.
Lemma 6.22**.**
FindWSΣ≤WΣ11-UCNN.
Proof.
Let T be a tree describing the complement of some open set, the payoff for
Player 1. Fix some strategy σ of Player 1. We understand this to
prescribe the action even at positions made impossible by σ itself.
For any v∈N∗ where Player 1 moves, consider the trees Tiv
describing the options available to Player 2 if the game starts at v,
Player 1 plays i and otherwise follows σ. σ is a winning
strategy iff for any v compatible with σ we find that
Tσ(v)v is well-founded. Only Σ11-UCNN is available here while a lot
of strategies may exist. We overcome this difficulty by considering the
optimal strategy, that is, the one that minimizes the rank of
Tσ(v)v.
Let v be a position where Player 1 moves. A certificate of optimality for
σ at v describes maps preserving ⊏ from Tσ(v)v
to Tiv∖{λ} (here λ denotes the empty sequence)
for every i<σ(v), and maps preserving ⊏ from
Tσ(v)v to Tjv for every j>σ(v). The set of strategies
σ and corresponding certificates of optimality for all positions is a
closed set computable from the game.
If we fix partial strategies of all proper extensions of v such that Player
1 can win from v, then there is a unique action of Player 1 at v such
that extending the strategy to v admits a certificate of optimality. It
follows that if Player 1 has a winning strategy, then there is a unique
strategy admitting a certificate of optimality at all compatible positions;
and this strategy is winning. We can compute this using
Σ11-UCNN.
∎
Given a Δ10-game G, we can compute the derived Δ10-game G′ where
the first player can decide whether to play G as Player 1, or as Player
2, and then proceed a play of a chosen side. Thus, Player 1 can
definitely win G′, and a winning strategy of Player 1 in G′ tells us
who wins G and how.
∎
Lemma 6.25**.**
FindWSΔ≤WFindWSΔ.
Proof.
Given a sequence G0,G1,… of Δ10-games all won by Player 1,
we combine them into a single Δ10 game where Player 2 first chooses n,
and then the players play Gn. Player 1 wins the combined game, and any
winning strategy in that game yields in the obvious way winning strategies
for every Gi.
∎
Let SB denote the space of Borel-truth values
(cf. [23, 40]). Roughly speaking, if p is a
Borel code of a Borel subset A of the singleton space {∙}, then
we think of p as a name of ⊤ (⊥, resp.) iff A=∅
(A=∅, resp.); if p is not a Borel code, p is not in the domain
of the representation.
Lemma 6.26**.**
(id:SB→2)≤WDetΔ.
Proof.
A Borel code can be viewed as a well-founded tree whose even-levels
(odd-levels, resp.) consist of ∃-vertices (∀-vertices,
resp.) and leaves are labeled by either ⊤ or ⊥ (corresponding to
either {∙} or ∅) [23, 40].
We can turn a SB-name into a Δ10-game by letting
Player 1 control the ∃-vertices, Player 2 the ∀-vertices,
make the ⊤-leaves winning for Player 1 and the ⊥-leaves losing.
Then Player 1 has a winning strategy iff the value of the root is ⊤.
Given a Nash equilibrium (σ,τ) we can compute the leaf reached by
the induced play, and find it to be equal to the truth value of the root.
∎
As shown in [40, Theorem 80], UCNN≤W(id:SB→2). By Lemma
6.26, the latter is reducible to DetΔ. This
is reducible to FindWSΔ by Lemma 6.24, which in
turn reduces to FindWSΔ by Lemma 6.25.
FindWSΔ≤WDetΔ is trivial, and so is FindWSΔ≤WFindWSΣ.
FindWSΣ≤WUCNN follows by Corollary 6.23.
∎
As in the case of the perfect tree theorem (Corollary 6.10), the results in this section can be viewed as a refinement of the following known result [3]:
Corollary 6.27**.**
For any open game, either the open player has a hyperarithmetical winning strategy or the closed player has a hyperlow winning strategy.
7 The two-sided versions of PTT and open determinacy
Rather than demanding a promise about the case of the theorem we are in, we could alternatively consider the task completely uniformly. As distinguishing the two cases is a Π11-complete question (cf. the well-known equation ⅁Σ10=Π11), the fully uniform task should not include the information in which case we are. A priori, since we considered two versions of listing, we also have the two corresponding version of the two-sided perfect tree theorem. We are left with the following formulations:
Definition 7.1**.**
wPTT2:Tr⇉Tr×NN has (T′,⟨b0p0,b1p1,b2p2,…⟩)∈wPTT2(T) iff one of the following
holds:
•
T′ is a perfect subtree of T;
•
[T]={pi∣bi=0}
Definition 7.2**.**
PTT2:Tr⇉Tr×NN has (T′,n⟨p0,p1,p2,…⟩)∈PTT2(T) iff one of the following holds:
•
T′ is a perfect subtree of T;
•
n=0, pi=pj for i=j and [T]={pi∣i∈N};
•
n>0, ∣[T]∣=n−1 and [T]={pi∣i<n−1}.
Definition 7.3**.**
DetΣ:O(NN)⇉NN×NN maps an open game W to a
pair of strategies σ, τ such that either σ is winning for
Player 1 or τ is winning for Player 2.
These variants are strictly harder than the non-uniform ones (which are
Weihrauch reducible to CNN by the results of Section
6). To see that, let χΠ11:NN→2 be the
characteristic function of a Π11-complete set. Since the single-valued
functions between computable Polish spaces which are Weihrauch reducible to
CNN are exactly those that are effectively Borel measurable
([6, Theorem 7.7]), and χΠ11 is not such, we have χΠ11≰WCNN.
Observation 7.4**.**
χΠ11≤WLPO′⋆wPTT2 and χΠ11≤WLPO⋆DetΣ.
Proof.
Deciding whether [T] is uncountable and who wins a Σ10-game are
Π11/Σ11-complete decision problems. Given trees T′ and T, we can
use LPO′ to decide whether or not T′ is a perfect subtree of T. Given
a Nash equilibrium (σ,τ) of a Σ10-game, we can compute the
induced play and then use LPO to decide who wins that play – and this is
the same player that has a winning strategy in the game.
∎
Corollary 7.5**.**
CNN<WwPTT2≤WPTT2 and CNN<WDetΣ.
Proof.
Using the fact that CNN is closed under composition [6, Corollary
7.6] we have χΠ11≰WCNN≡WLPO⋆CNN≡WLPO′⋆CNN.
∎
In particular, we find that FindWSΣ<WDetΣ and FindWSΠ<WDetΣ.
Thus, knowing who wins a Σ10-game makes it strictly easier to find a Nash
equilibrium. This is in contrast to Δ10-games (as seen in Theorem
6.21), as well as to games on Cantor space with winning
sets in the difference hierarchy over Σ10 (cf. [31]).
Knowing who wins the game allows for constructions such as the one used in
Lemma 6.25 to conclude that finding a winning
strategy is parallelizable (i.e. FindWSΣ≡WFindWSΣ and
FindWSΠ≡WFindWSΠ). We will see in Corollary
7.13 below that this is not just an obstacle for the
proof strategy, but that the result differs for DetΣ.
If then else
As we have seen, many theorems equivalent to ATR0 are described as
dichotomy-type theorems: Exactly one of A or B holds. Thus, it is
natural to consider the following if-then-else problem for a given dichotomy
A xor B: Provide two descriptions (α,β) trying to verify A
and B simultaneously. If A is true, then α is a correct proof
validating A; or else β is a correct proof of B, where we do not
need to know which one is correct. We formalize this idea as follows.
A space of truth values is just a represented space B with underlying set {⊤,⊥}.
Definition 7.6**.**
Let B be a space of truth values. For f:⊆X⇉Y and g:⊆A⇉B, we define
[TABLE]
via (b,x0,x1)∈dom([if B then f else g]) iff b=⊤ and x0∈dom(f) or b=⊥ and x1∈dom(g), and (y0,y1)∈[if B then f else g](b,x0,x1) iff b=⊤ and y0∈f(x0) or b=⊥ and y1∈g(x1).
Note that the degree of [if B then f else g] depends on the precise
choice of spaces for domain and codomains involved, beyond what matters for
where f and g are actually defined and are taking their range. In
particular, [if B then f else g] is not an operation on Weihrauch
degrees777Let X be the represented space of the
non-computable elements of NN, and f:⊆NN→NN the
restriction of idNN to the non-computable elements (idX
and f are the same function, but defined on different spaces); then
idX≡Wf, yet [if S then f else idNN]≰W[if S then idX else idNN] because the former has computable
inputs while the latter does not..
The upper bound
Let SΣ11 be the space of truth values where p is a name for
⊤ iff p codes an ill-founded tree, and a name for ⊥ iff it codes
a well-founded tree.
In the proofs of Propositions 6.3 and 6.19, we
constructed closed sets containing information over the perfect subtrees or
the winning strategies of Player 2 respectively. In particular, by testing
whether these are empty or not, we can decide in which case we are, and
obtain the answer in SΣ11. Thus, by combining Proposition
6.3 and Theorem 6.4, respectively Proposition
6.19 and Theorem 6.21, we obtain the
following:
Corollary 7.7**.**
PTT2≤W[if SΣ11 then CNN else UCNN].
Corollary 7.8**.**
DetΣ≤W[if SΣ11 then CNN else UCNN].
As UCNN≤WCNN, it follows that
[if SΣ11 then CNN else UCNN]≤WCNN⋆χΠ11. In
particular, the difference between
[if SΣ11 then CNN else UCNN] and CNN disappears if we
move from Weihrauch reducibility to computable reducibility. It follows
immediately that Gandy’s basis theorem applies to DetΣ: Every Σ10-game
has a Nash equilibrium that is hyperlow relative to the game.
Idempotency
We can show a kind of absorption result for the if-then-else construction.
Recall that NHA asks for an output that is not hyperarithmetic
relative to the input.
Proposition 7.9**.**
Let g have a hyperarithmetical point ρ in
its codomain. If we have f×NHA≤W[if B then g else UCNN], then f≤Wg.
Proof.
Any x∈dom(f) is provided in the form of some name px, which is a
valid input to NHA. If some (x,px)∈dom(f×NHA) were mapped to some (⊥,a,A) via the reduction, then A={q} where q is hyperarithmetical in px. Then (ρ,q) is a valid
output of [if B then g else UCNN], but we cannot compute a solution
to NHA(px) from (ρ,q).
Thus, every (x,px) gets mapped to (⊤,ax,A) such that from b∈g(ax) we can compute y∈f(x) (since (b,z) for any z, say
(b,∅), is a solution to the instance (⊤,ax,A)). This provides
the claimed reduction f≤Wg.
∎
By Corollaries 7.5, 7.8 and
7.7, and Proposition 7.9 we get
the following:
Corollary 7.10**.**
wPTT2×NHA≰W[if SΣ11 then CNN else UCNN].
Corollary 7.11**.**
DetΣ×NHA≰W[if SΣ11 then CNN else UCNN].
Using the corollaries above in conjunction with Corollary
3.6, we obtain:
Corollary 7.12**.**
wPTT2×CNN≰WPTT2 and hence wPTT2×wPTT2≰WPTT2.
Corollary 7.13**.**
DetΣ×CNN≰WDetΣ and hence DetΣ×DetΣ≰WDetΣ.
Products with UCNN
While we just saw that DetΣ, PTT2 and
[if SΣ11 then CNN else UCNN] are not closed under products
with CNN, the situation for products with UCNN is different:
Proposition 7.14**.**
UCNN×[if B then CNN else UCNN]≡W[if B then CNN else UCNN] for any space of truth values
B.
Proof.
Let {a}, b∈B, A, B be the input to UCNN×[if B then CNN else UCNN]. We can use
[if B then CNN else UCNN] on b, {a}×A and {a}×B, as {a}×A is non-empty iff A is, and {a}×B
is a singleton iff B is. We will receive as output (⟨p,x⟩,⟨q,y⟩) such that ⟨x,y⟩ is a valid output to
[if B then CNN else UCNN](b,A,B), and at least one of p and q
is a. Let us write p≤n for the prefix of p of length n+1. We
have that, if p≤n=q≤n, then p≤n=a≤n, and
if p≤n=q≤n, then either p∈/{a} or q∈/{a}, hence we can compute a from p, q and {a}.
∎
Proposition 7.15**.**
UCNN×PTT2≡WPTT2.
Proof.
Let ({a},T) be the input to UCNN×PTT2. From this input we
can build a tree T0 such that [T0]={a}×({0ω}∪1[T]) (notice that ∣[T0]∣=∣[T]∣+1). PTT2(T0) yields a tree T′ and
a sequence n⟨(q0,t0p0),(q1,t1p1),…⟩.
We first explain how to compute the sequence part of PTT2(T). If n=1,
or n=0 and more than one ti is [math], or n>1 and more than one ti
for i<n−1 is [math], then the sequence is not listing [T0] (because
[T0]=∅ and (a,0ω) is the only member of [T0] whose
second component starts with [math]), which implies that [T0], and hence
[T], was uncountable. In this case, we can just output some arbitrary
sequence. Otherwise let pi′ be the sequence consisting of the odd digits
of pi. If n=0, we output 0⟨pi0′,pi1′,…⟩ where the ik are the (all but one) indices such that ti=0
(in this way, if ⟨(q0,t0p0),(q1,t1p1),…⟩ lists
injectively [T0], our output lists injectively [T]). To achieve the same
result when n>1 we output (n−1)⟨pi0′,pi1′,…⟩ where we are omitting the (at most one) i<n−1 such that ti=0.
To compute the tree part of PTT2(T), starting from T′ we obtain a tree
T′′ as follows: On the first three levels (corresponding to the first two
digits of a and the control bit), go down some arbitrary edge in T′. Then
alternate adding all children of the present vertices into T′′, and passing
down some arbitrary edge. If T′ is perfect, then so is T′′, and moreover,
T′′⊆T in that case.
We need also to compute a. To produce a possible candidate, we attempt to
compute the left-most branch q of T′. If we ever reach a leaf (which
never happens if T′ is perfect), then we continue q by constant [math]. In
any case, let q′ be the even digits of q: if T′ is a perfect subtree of
T0 then a=q′. On the other hand, if (q0,t0p0),(q1,t1p1),…⟩ lists [T0] then a=q0. Thus a=q0 or a=q′. As in
the proof of Proposition 7.14 it follows that we can
compute a from q0, q′ and {a}.
∎
Proposition 7.16**.**
UCNN×DetΣ≡WDetΣ.
Proof.
By Theorem 6.21, we have UCNN≤WFindWSΔ, i.e. we
can compute a Δ10-game G1′ from {a} such that Player 1 wins
G1′, and from a winning strategy of Player 1 in G1′ we can compute
a. Let G2′ be the game with the roles of Player 1 and Player 2
exchanged, which is still Δ10. Now we construct a Σ10 game G′′ from a
Σ10-game G, and from G1′ and G2′.
The players start playing G and G2′ in parallel. If Player 2 wins both
of these, he wins in G′′. Else, if he loses one of them (which would happen
at some finite time), the players proceed to play G1′, and whoever wins
G1′ wins G′′. W.l.o.g. we assume that Player 2 can choose to lose G
right at the start of G′′.
Since by assumption Player 2 has a winning strategy in G2′, and Player
1 has a winning strategy in G1′, the winning strategies of Player 2
are exactly those that consists of playing winning strategies in G and
G2′ simultaneously. On the other hand, Player 1 can win the game for
sure only by first playing a winning strategy in G (and arbitrarily in
G2′), followed by a winning strategy in G1′.
From a Nash equilibrium of the whole game we thus obtain a Nash equilibrium
in G by considering how the players play in G. Furthermore, we consider
how Player 1 plays in the copy of G1′ played when Player 2 loses in
G right at the start of G′′, and how Player 2 plays in G2′, and
compute two candidates q0, q1 for a from that. As in the proof of
Proposition 7.14, we can then compute a from {a},
q0 and q1.
∎
Here the difference between wPTT2 and PTT2 is revealed, as the former
is more sensitive to products. We recall that a Weihrauch degree is called
fractal, if it has a representative f:⊆NN⇉NN
such that for any w∈N<N such that wNN∩dom(f)=∅ it holds that f∣wNN≡Wf. Most of the degrees
considered in this articles are fractals, including wPTT2.
Proposition 7.17**.**
If f is a fractal and LPO×f≤WwPTT2, then f≤WCNN.
Proof.
W.l.o.g. assume that f:⊆NN⇉NN witnesses its own
fractality.
Fix a reduction of LPO×f to wPTT2 and let K1 be the
computable function that transforms the output of wPTT2 and the original
input of LPO×f into the answer to the LPO-instance. We
distinguish the following cases:
There exists 0n, w∈N<N, a finite tree T, and a finite
prefix of a list ⟨0q0,0q1,0q2,…⟩ such that K1
provides its answer upon reading those (as input for LPO, input for
f, first and second component of the output of wPTT2, in that
order).
Then by fixing the input to LPO to something consistent with 0n and
incompatible with the answer provided, we can make sure that the reduction
needs to avoid the prefix to be valid for any input to f extending w.
But this can only be achieved by making the input to wPTT2 having
uncountable body and not having T as prefix of any perfect subtree. This
means in particular that we are dealing with an input to PTT1. As f is
a fractal, restricting to those of its inputs extending w does not
decrease its Weihrauch degree, and we conclude f≤WCNN.
2. 2.
For no 0n, w∈N<N, finite tree T, and finite prefix of
a list ⟨0q0,0q1,0q2,…⟩, K1 provides its
answer upon reading those.
If we fix the LPO-input to be 0ω, we see that to ensure that
K1 behaves correctly, the list-component of the output of wPTT2 must
actually list some elements. This can only be guaranteed if the input to
wPTT2 is a tree with countable non-empty body, i.e. is already in the
domain of List. We thus conclude f≤WList≡WUCNN (by
Theorem 6.4) and, a fortiori, f≤WCNN.∎
Corollary 7.18**.**
LPO×wPTT2≰WwPTT2.
Corollary 7.19**.**
wPTT2<WPTT2.
Proof.
By contrasting Corollary 7.18 and Proposition 7.15.
∎
We shall see that wPTT2 is still closed under some non-trivial products.
For that, let NON:2N⇉2N be defined via q∈NON(p) iff q≰Tp; i.e. NON is the
function corresponding to the theorem asserting the existence of sets
non-computable in any given set.
Proposition 7.20**.**
NON×wPTT2≤WwPTT2.
Proof.
Fix a Turing functional Φ such that for every p∈2N, Φp is
an injective enumeration of p′, the Turing jump of p. Let p^∈NN be such that for every n we have that p^(n)=0 implies n∈/p′ and p^(n)>0 implies Φp(p(n)−1)=n. Then p^ is
Turing equivalent to p′ and hence p^≰Tp.
Notice that the function from 2N to A(NN) which sends p to
{p^} is computable. Therefore, from (p,A)∈2N×A(NN) we can compute {p^}×({0ω}∪1A)∈A(NN). From any solution to wPTT2({p^}×({0ω}∪1A)) we can compute a solution to wPTT2(A) with the
argument of the first part of the proof of Proposition
7.15. Moreover, any solution to wPTT2({p^}×({0ω}∪1A)) is ≥Tp^, and hence solves
NON(p).
∎
In [19], products with LPO and NON are used to
separate Weihrauch degrees in a similar fashion.
8 TCNN – a candidate for ATR0?
Our separation proofs of principles like DetΣ and
PTT2 from CNN relied on being able to transform an arbitrary closed
subset into an input for the former, with specified behaviour occurring only
for non-empty closed sets. We can capture this using the notion of
total continuation of closed choice on NN:
Definition 8.1**.**
Let TCNN:A(NN)⇉NN be defined via p∈TCNN(A) iff A=∅⇒p∈A.
In the same vein, we can define the total continuation of other choice
principles. The computable compactness of 2N yields TC2N≡WC2N. The principle TCN was studied in [33].
Proposition 8.2**.**
CNN<WTCNN;
2. 2.
TCNN<WLPO×TCNN.
3. 3.
If NON×f≤WTCNN, then f≤WCNN;
4. 4.
TCNN<WwPTT2;
5. 5.
TCNN<WDetΣ;
6. 6.
[if SΣ11 then CNN else UCNN]<WTCNN×CNN.
Proof.
The reduction is trivial. Separation follows from LPO⋆CNN≡WCNN and χΠ11≤WLPO⋆TCNN (the latter is
straightforward because LPO can check whether the output of
TCNN(A) belongs to A).
2. 2.
Again, the reduction is trivial. For the separation, assume that
LPO×TCNN≤WTCNN via computable H, K1, K2.
Recall that LPO(r)=1 iff r=0ω. Consider the input 0ω
for LPO and NN∈A(NN) (coded as some name t)
for TCNN on the left. There has to be some p∈NN such that
K1(0ω,t,p)=1. By continuity, we find that K1(0kq,t≤kt′,p)=1 for sufficiently large k and arbitrary q, t′.
For any A∈A(NN) we can compute some name of the form
t≤kt′. Now consider what happens if the inputs on the left are
0k1ω and some t≤kt′: If H(0k1ω,t≤kt′)
ever returns a name for the empty set, then p is a valid solution to
TCNN on the right. But then K1 will answer incorrectly 1. Thus,
H(0k1ω,t≤kt′) never returns a name for the empty set. But
then we obtain a reduction TCNN≤WCNN, contradicting (1).
3. 3.
As TCNN(∅) has computable solutions, the reduction
NON×f≤WTCNN already has to be a reduction to
CNN.
4. 4.
The reduction given in Proposition 6.3 works for this, by
using the following observation: given A∈A(NN), T∈Tr such that [T]=A×NN and (T′,⟨b0p0,b1p1,…⟩)∈PTT2(T), if we realize that T′ is
not pruned (which can happen only if A=∅) we can continue
our output with 0ω.
Strictness follows by (3), Proposition 7.20 and
Corollary 7.5.
5. 5.
The reduction given in Proposition 6.19 works for
this, by using the following observation: if A=∅ then
Player 1 has a winning strategy in the Σ10 game we constructed (in
fact, any strategy for 1 is winning), however following the strategy
for 2 provided by DetΣ we find an element of TCNN(A).
Strictness follows by (2), Proposition 7.16 and
Corollary 7.5.
6. 6.
The arguments used to establish Lemma 6.7 or
6.22 show that the total continuation TUCNN of
UCNN (i.e. the total multivalued function defined on
A(NN) which extends UCNN and is defined as NN
on non-singletons) is reducible to CNN. For example, given an
arbitrary closed A⊆NN we can compute the nonempty
Σ11 set of the mCB-certificates of A and, choosing an
element in it, compute the list of the elements of A whenever A is
a countable, and in particular a singleton.
Thus, we can consider TCNN×TUCNN in place of TCNN×CNN. Given some input b,A,B to
[if SΣ11 then CNN else UCNN] we ignore b, we feed
A to TCNN, and B to TUCNN. Any resulting output pair is
a valid output to [if SΣ11 then CNN else UCNN].
To see that TCNN×CNN≡W[if SΣ11 then CNN else UCNN] first notice that
TCNN×CNN×CNN≡WTCNN×CNN. On the other hand, we have
[TABLE]
otherwise, since by Corollaries 7.7 and
3.6 we have PTT2≤W[if SΣ11 then CNN else UCNN] and NHA≤WCNN, we would have PTT2×NHA≤W[if SΣ11 then CNN else UCNN] and Proposition
7.9 would imply PTT2≤WCNN, against
Corollary 7.5.∎
Corollary 8.3**.**
PTT2∗≡WDetΣ∗≡WTCNN∗.
Proof.
TCNN∗≤WPTT2∗ is immediate from Proposition 8.2(4). On
the other hand we have
It is reasonable to expect a Weihrauch degree corresponding to an axiom
system from reverse mathematics to be closed under finite parallelization.
For candidates for WKL0 or ACA0 this happens
inherently. Here, we might need to demand it explicitly, and thus consider
the degree TCNN∗ rather than any directly defined one to be one of the
most promising candidates.
A potentially convenient way to think about the separation between CNN
and TCNN is in terms of translations between truth values. TCNN
allows us to treat a single Π11-set as an open set, whereas CNN
cannot even bridge the gap from Σ11 to Borel.
Proposition 8.4**.**
(id:SΠ11→S)≤WTCNN, but
(id:SΣ11→SB)≰WCNN.
Proof.
For the reduction, we observe that A=∅ iff p∈/A for some
p∈TCNN(A).
For the non-reduction, we recall that id:SB→2≤WUCNN was shown in [40, Lemma 79], and that
UCNN⋆CNN≡WCNN as shown in [6, Theorem 7.3].
Thus, assuming the reduction would hold, we would even have that (id:SΠ11→2)≤WCNN, which
contradicts [6, Theorem 7.7] because the unique realizer of id:SΠ11→2 is not effectively Borel measurable.
∎
Next, we shall see that the additional computational power of TCNN
(even of its parallelization TCNN) over UCNN concerns
only multivalued problems.
Theorem 8.5**.**
The following are equivalent for single-valued f:⊆X→NN where X is a represented space:
f≤WUCNN;
2. 2.
f≤WTCNN.
Proof.
That 1 implies 2 is trivial. For the other direction, we first argue that it suffices to consider single-valued f:⊆NN→{0,1}. Then we show that for
single-valued f:⊆NN→{0,1}, f≤sWTCNN
implies f≤WΔ11-CA and invoke Theorem 3.11.
Let δX be the representation of X. For f:X→NN, consider the map F:⊆NN→{0,1} where
F(nmp)=1 if f(δX(p))(n)=m and F(nmp)=0 otherwise,
provided p∈dom(fδX). Now it holds that F≤Wf≤WF (the latter reduction holds because f is single-valued). As
UCNN is parallelizable, F≤WUCNN is equivalent to
F≤WUCNN and hence f≤WUCNN.
For the second claim, we can start from a strong Weihrauch reduction because
TCNN is a cylinder. Assume that f:⊆NN→{0,1} and f≤sWTCNN via computable K, H. The outer reduction witness K
essentially consists of two open sets U0,U1∈O((NN)N),
while the inner reduction witness H gives us for each p∈NN a
sequence (An(p))n∈N of closed sets. For S⊆N and U∈O((NN)N), let πS(U) denote the projection of U to
the components in S. Now we find that:
[TABLE]
(Notice that ∏n∈NAn(p)⊆Ub does not imply f(p)=b in general because some of the An(p) could be empty.) This is a
Π11-condition. Since exactly one of f(p)=0 and f(p)=1 holds, we
thus have a valid instance for Δ11-CA.
∎
In particular, TCNN does not reach the level of
Π11\mbox−CA0.
Corollary 8.6**.**
χΠ11≰WTCNN.
9 Open questions and discussion
The results reported in Section 7 immediately lead to three interlinked questions, which unfortunately we have been unable to resolve so far:
Question 9.1**.**
Does DetΣ≡W[if SΣ11 then CNN else UCNN]?
Question 9.2**.**
Does PTT2≡W[if SΣ11 then CNN else UCNN]?
Question 9.3**.**
How do PTT2 and DetΣ relate?
We would expect that other theorems equivalent to ATR0 (e.g. open Ramsey) exhibit similar behaviour, i.e. a non-constructive disjunction
between cases equivalent to CNN and UCNN respectively. Proving
any reductions between the two-sided versions of these theorems could be very
illuminating. Until then, we might have to settle for classifications in the
Weihrauch lattice up to ∗, and strive to understand better the degree
TCNN∗.
Brattka has also raised the question whether the strong two-sided versions,
which return an answer on the applicable case together with a witness, are
worthwhile studying. It seems conceivable that finding reductions here would
be easier. Up to ∗, these problems would have the degree TCNN∗×χΠ11∗. Would this be an acceptable candidate for an
ATR0-equivalent, or is this degree too close to
Π11\mbox−CA0?
Given that TCNN∗ is not closed under composition, one could make the
case that TCNN⋄ (its closure under generalized register
machines, cf. [33]) is the better candidate. Note that
TCNN⋄≡W(TCNN×χΠ11)⋄,
so the distinction between the weak and strong two-sided versions of the
theorems would disappear here. How well justified this step would be in
particular depends on whether there exists a natural theorem equivalent to
ATR0 in reverse mathematics where ATR0 is actually
used in a sequential way, i.e. a theorem naturally associated with a
Weihrauch degree not reducible to TCNN∗.
Acknowledgements
In the earlier stages of this research Marcone collaborated with Andrea Cettolo, and some of the proofs were obtained jointly with him. Pauly began working on this project while being a visiting fellow at the Isaac Newton Institute for Mathematical Sciences in the programme ‘Mathematical, Foundational and Computational Aspects of the Higher Infinite’. He thanks Vasco Brattka, Jun Le Goh, Luca San Mauro and Richard Shore for inspiring conversations. The research project benefitted from discussion at the Dagstuhl seminars 15392 ‘Measuring the Complexity of Computational Content: Weihrauch Reducibility and Reverse Analysis’ and 18361 ‘Measuring the Complexity of Computational Content: From Combinatorial Problems to Analysis’.
Kihara’s research was partially supported by JSPS KAKENHI Grant 17H06738, 15H03634, and the JSPS Core-to-Core Program (A. Advanced Research Networks).
Marcone’s research was partially supported by PRIN 2012 Grant “Logica, Modelli e Insiemi” and by the departmental PRID funding “HiWei — The higher levels of the Weihrauch hierarchy”.
Pauly has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 731143, Computing with Infinite Data.
Bibliography45
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[1]
2[2] Laurent Bienvenu, Noam Greenberg & Benoit Monin (2017): Continuous higher randomness . J. Math. Log. 17(1), pp. 1750004, 53, 10.1142/S 0219061317500040 . · doi ↗
3[3] Andreas Blass (1972): Complexity of winning strategies . Discrete Mathematics 3, pp. 295–300, 10.1016/0012-365X(72)90086-6 . · doi ↗
4[4] Vasco Brattka (2005): Effective Borel measurability and reducibility of functions . Mathematical Logic Quarterly 51, pp. 19–44, 10.1002/malq.200310125 . · doi ↗
5[5] Vasco Brattka (2018): A Galois connection between Turing jumps and limits . Logical Methods in Computer Science 14(3), 10.23638/LMCS-14(3:13)2018 . · doi ↗
6[6] Vasco Brattka, Matthew de Brecht & Arno Pauly (2012): Closed Choice and a Uniform Low Basis Theorem . Annals of Pure and Applied Logic 163(8), pp. 968–1008, 10.1016/j.apal.2011.12.020 . · doi ↗
7[7] Vasco Brattka & Guido Gherardi (2011): Effective Choice and Boundedness Principles in Computable Analysis . Bulletin of Symbolic Logic 17, pp. 73–117, 10.2178/bsl/1294186663 . Available at http://arxiv.org/abs/0905.4685 . · doi ↗
8[8] Vasco Brattka & Guido Gherardi (2011): Weihrauch Degrees, Omniscience Principles and Weak Computability . Journal of Symbolic Logic 76, pp. 143–176, 10.2178/jsl/1294170993 . Available at http://arxiv.org/abs/0905.4679 . · doi ↗