Lipschitz and Wadge binary games in second order arithmetic

Lipschitz and Wadge binary games in second order arithmetic Andrés Cordón-Franco a, F. Félix Lara-Martín a,∗, Manuel J.S. Loureiro b aDpto. Ciencias de la Computación e Inteligencia Artificial, Facultad de Matemáticas, Universidad de Sevilla, C/ Tarfia, s/n, 41012 Sevilla, Spain bFaculty of Engineering, Lusofona University, Campo Grande 376, 1749-024 Lisbon, Portugal a b s t r a c t MSC: 03B30 03E60 03F35 03E15 Keywords: Reverse mathematics Determinacy Wadge games Semilinear ordering principle We present a detailed formalization of Lipschitz and Wadge games in the context of second order arithmetic and we investigate the logical strength of Lipschitz and Wadge determinacy, and the tightly related Semi-Linear Ordering principle, for the first levels of the Hausdorff difference hierarchy in the Cantor space. As a result, we obtain characterizations of WKL0and ACA0in terms of these determinacy principles. 1. Introduction Lipschitz and Wadge games were first introduced in descriptive set theory in the late 1960’s by W.W. Wadge (see [16]) as a tool for studying the relative complexity of subsets of the Baire space ωω. Given subsets Aand B, Ais said to be Wadge reducible to B, in symbols A ≤WB, if there is a continuous function F such that x ∈Aif, and only if, F(x) ∈B(the problem of verifying membership in Acan be reduced to the problem of verifying membership in Band so Ais, in a certain sense, no more complicated than B). In a similar way, Ais said to be Lipschitz reducible to B, in symbols A ≤LB, if the previous function Fis required to be a Lipschitz function. Wadge proved that the reducibility relations ≤Wand ≤Lcan be naturally studied in terms of the so-called Wadge and Lipschitz games. These are two person infinite games with perfect information in which each player has a different pay-off set Aand B, respectively, and player *Corresponding author. E-mail addresses: [email protected] (A. Cordón-Franco), ffl[email protected] (F.F. Lara-Martín), [email protected] (M.J.S. Loureiro). https://doi.org/10.1016/j.apal.2023.103301 . 2 II wins the game if she mimics player I’s resulting play, that is, if she plays inside Bif and only if player I plays inside A(see section 2for a precise definition of these games). Wadge then assumed determinacy for Wadge and Lipschitz games as a working hypothesis and he extensively studied the structure of the equivalence classes generated by ≤Wand ≤Lin the Baire space, especially of those equivalence classes formed by Borel sets. In particular, he derived the following somewhat surprising comparability property, known as the Semi-Linear Ordering principle: (SLO) = “For all subsets Aand B, either Ais reducible to Bor the complement of Bis reducible to A.” Since then the use of Wadge/Lipschitz games has been shown to be a useful tool in descriptive set theory and many authors have contributed to this line of research. The reverse mathematics of the determinacy of general two person infinite games has been thoroughly investigated by, among others, J.R. Steel, K. Tanaka, M.O. MedSalem, and T. Nemoto ([13], [14], [15], [10], [9]). As a result, we now have a detailed level-by-level analysis of the logical strength of these determinacy principles both in the Baire space ωωand in the Cantor space 2ωand, in most cases, their exact strength has been calibrated in terms of subsystems of second order arithmetic. In contrast, the situation for Lipschitz and Wadge determinacy is completely different. By a remarkable result of A. Louveau and J. Saint Raymond [6]we know that full second order arithmetic Z2proves Borel Wadge/Lipschitz determinacy, but no detailed analysis of the strength of Lipschitz or Wadge determinacy in terms of subsystems of second order arithmetic can be found in the literature and, to the best of our knowledge, the reverse mathematics of the semi-linear ordering principle SLO has not been systematically investigated either. A first step towards filling this gap was M.J.S. Loureiro’s Ph.D. thesis [5], where the author systematically studied the reverse mathematics of Wadge/Lipschitz determinacy and SLO for the first levels of the Borel hierarchy both in the Baire space and in the Cantor space. In [5]the author was able to characterize the central second arithmetic theories ACA0and ATR0using these determinacy principles, and he raised the question of characterizing the system WKL0in terms of Lipschitz determinacy in the Cantor space. Let us introduce some terminology in order to state more precisely these results. Given two formula classes Γ1and Γ2in the language of second order arithmetic, let (Γ1, Γ2)-Det∗ L/W denote the principle of Lipschitz/Wadge determinacy for games in the Cantor space where player I’s pay-off set is Γ1-definable and player II’s pay-off set is Γ2-definable. Likewise, let (Γ1, Γ2)-SLO∗ L/W denote the corresponding semi-linear ordering principle in the Cantor space. Finally, we will write (Γ1, Γ2)-DetL/W and (Γ1, Γ2)-SLOL/W for the corresponding principles in the Baire space (we refer the reader to sections 2and 5for a detailed formalization of these principles in the language of second order arithmetic). The main results of [5]are the following (note that we will simply write Γ-Det(∗) L/W or Γ-SLO(∗) L/W if Γ1=Γ 2=Γ). Theorem 1.1. (Theorem 4.12, Proposition 4.18, Corollary 4.42, Theorem 5.1, Theorem 5.28, Theorem 4.37 and Proposition 5.33 in [5]) 1. RCA0proves Δ0 1-Det∗ W, and WKL0proves (Δ0 1, Σ0 1)-Det∗ L/W and (Σ0 1, Δ0 1)-Det∗ L. 2. Over RCA0, (Σ0 1∧Π0 1)-Det∗ L, (Σ0 1∧Π0 1)-SLO∗ Land ACA0are pairwise equivalent. 3. Over ACA0, Δ0 1-DetL, Δ0 1-SLOLand ATR0are pairwise equivalent. 4. Over RCA0, Σ0 1-DetL, (Δ0 1, Σ0 1)-DetLand ATR0are pairwise equivalent. 5. Let Γ =Σ 0 1∧Π0 1. Then, ACA0proves Γ-Det∗ Wand Π1 1-CA0proves (Γ ∪¬Γ)-DetL/W . Also, the following question was left pending in [5]: Problem 1. (Problem 4.17 in [5]) Is WKL0equivalent over RCA0to Δ0 1-Det∗ L? 3 In preparing the final version of the present paper, we have learned that W. Chan, possibly following a suggestion of T. Nemoto, had also considered it interesting to develop a more detailed analysis of Borel Wadge/Lipschitz determinacy in terms of subsystems of second order arithmetic already in 2011-2012, although his work in this direction had remained unpublished. Nevertheless, motivated by the aforementioned question on WKL0posed in [5], in his recent work [4]Chan has proved WKL0to be equivalent to a certain weak form of Lipschitz determinacy in the Cantor space, thus giving a first partial answer to that question. More precisely, Theorem 1.2. ([4]) Over RCA0, (Σ0 1∧Π0 1, Δ0 1)-Det∗ Land RCA0are pairwise equivalent. The current paper builds on the work in [5]and presents extensions and improved versions of the main results in [5] concerning the Cantor space (a second paper dealing with Lipschitz/Wadge determinacy and SLO in the Baire space is in preparation). Most remarkably, we give a complete answer to Problem 1 above by showing that Δ0 1-Det∗ Lalready implies WKL0over RCA0, and we improve the reversals for ACA0 previously obtained in [5]. The following theorem summarizes the main results we prove in this paper. Theorem 1.3. 1. RCA0proves (Δ0 1, Σ0 n)-Det∗ W, (Δ0 1, Σ0 n)-SLO∗ Wand (Σ0 n, Δ0 1)-SLO∗ W, for n >0. 2. Over RCA0, Δ0 1-Det∗ L, (Δ0 1, Σ0 1)-Det∗ L, (Σ0 1, Δ0 1)-Det∗ Land WKL0are pairwise equivalent. 3. Over WKL0, Σ0 1-Det∗ L/W , Σ0 1-SLO∗ L/W and ACA0are pairwise equivalent. 4. Over RCA0, Σ0 1-Det∗ L, (Σ0 1, Σ0 1∧Π0 1)-Det∗ L/W , (Σ0 1, Σ0 1∧Π0 1)-SLO∗ L/W and ACA0are pairwise equivalent. Some remarks concerning Theorem 1.3 are in order. Firstly, it is important to note that the implications from WKL0and ACA0to Lipschitz determinacy statements can also be derived from previous general results on determinacy obtained by Nemoto, MedSalem and Tanaka in [10]and [9]. This is because every Lipschitz game can be effectively reduced to a general two person infinite game. Roughly speaking, one can infer Lipschitz determinacy for Γsets from general determinacy for (Γ ∧¬Γ) sets (see Remark 2.4 for details). This reduction provides us with some upper bounds on the strength of Lipschitz determinacy but, in general, these upper bounds need not be optimal. Actually, this will be the case for higher levels of the Borel hierarchy, as by the aforementioned result of A. Louveau and J. Saint Raymond Z2proves Borel Lipschitz determinacy whereas by a result of D. Martin [7], Z2does not prove general Σ0 4-determinacy (this result was improved by A. Montalbán and R.A. Shore [8]showing that Z2does not prove general Δ0 4-determinacy). This justifies the methodology used in the present paper: we give explicit formalizations of Lipschitz and Wadge games in second order arithmetic, and we give direct proofs of Lipschitz and Wadge determinacy with no use of previously known results on general determinacy. In fact, we show that the topological analysis of the complete sets in the first levels of the Hausdorff difference hierarchy developed in [16]can be adapted to prove the determinacy of Lipschitz/Wadge games of those complexities (recall that in [16]the author was not concerned with proving determinacy results but he assumed determinacy of Lipschitz and Wadge games as an initial hypothesis for his work). The use of topological arguments makes, we think, our determinacy proofs conceptually simple: very roughly speaking, the player who plays in a pay-off set of richer topological structure will win the game. Secondly, let us observe that the implications from RCA0, WKL0and ACA0to Wadge determinacy statements in Theorem 1.3 are new results, in the sense that they do not follow from previous general results on determinacy (Wadge determinacy for Γsets can be naturally reduced to general determinacy for max{Σ0 2, Γ ∧¬Γ}sets, see Remark 2.4) The proofs of these implications can also be found in the Ph.D. thesis [5] (unpublished). 4 Finally, it should be noted that the reversals for WKL0and ACA0in Theorem 1.3 are genuinely new results. On the one hand, they cannot be deduced from (and, indeed, can be seen as reinforcements of) previous general results on determinacy obtained in [10]and [9], for Lipschitz/Wadge determinacy and SLO are formally weaker principles than general determinacy. On the other hand, our reversal for the Weak Köning Lemma (namely, Δ0 1-Det∗ Limplies WKL0over RCA0) is stronger than the one obtained in [4], where the author needed (Σ0 1∧Π0 1, Δ0 1)-Det∗ Lto recover WKL0over RCA0. In a similar vein, our reversals for Arithmetical Comprehension (namely, Σ0 1-Det∗ Land (Σ0 1, Σ0 1∧Π0 1)-SLO∗ L/W imply ACA0over RCA0) are stronger than the ones obtained in [5], where (Σ0 1∧Π0 1)-Det∗ Lor (Σ0 1∧Π0 1)-SLO∗ Lare needed to recover ACA0 over RCA0. The paper is divided into six sections. Section 1is introductory. Section 2contains some preliminaries and describes a detailed formalization of Lipschitz and Wadge games in second order arithmetic. Although in this paper we shall only deal with games in the Cantor space, we have preferred to present this formalization in the more general setting where players I and II play in the space XNwith X⊆N, as this could be useful for future references. Section 3is devoted to the study of clopen Lipschitz/Wadge determinacy and contains a reversal for WKL0in terms of clopen Lipschitz determinacy. In section 4we show that ACA0proves open Lipschitz/Wadge determinacy in the Cantor space, and we prove a combinatorial version of a result of P. Shafer [11] stating that ACA0is equivalent to the topological property: “every closed and not open set in the Cantor space has nonempty boundary.” Reversals for ACA0are postponed until section 5, in which we initiate the study of the reverse mathematics of the semi-linear ordering principle SLO and we establish two reversals for ACA0in terms of this principle. Section 6contains some concluding remarks. 2. Lipschitz and Wadge games in second order arithmetic We assume familiarity with subtheories of second-order arithmetic, as presented in [12]. Of the “big five” theories thoroughly studied in that book, here we will only deal with the three weakest: RCA0⊂WKL0⊂ ACA0. The theory of recursive comprehension RCA0is axiomatized (over a finite set of basic axioms) by Δ0 1 comprehension and Σ0 1induction. We will use RCA0as our base theory through this paper. The axioms of WKL0are those of RCA0plus weak Köning’s lemma stating that every infinite binary tree has a path. The theory ACA0extends RCA0by arithmetical comprehension. Our notation and terminology are standard and follow [12](for details and full technical background the reader should consult that book). Here we restrict ourselves to recalling some basic notions concerning functions and finite sequences that will be used extensively in this paper. Within RCA0, we define Nto be the unique set Xsuch that ∀n (n ∈X)and we define a numerical paring function by letting (m, n) = (m +n)2+m. Using Δ0 1comprehension, we can prove that for all sets X, Y⊆N, there exists a set X×Y⊆N consisting of all (m, n)such that m ∈Xand n ∈Y. A function f:X→Yis defined to be a set f⊆X×Y such that for all m ∈Xthere is exactly one n ∈Ysuch that (m, n) ∈f. For m ∈X, f(m)is defined to be the unique nsuch that (m, n) ∈f. We write f∈XNto mean that fis a function from Nto X, although the set XNdoes not formally exist within second order arithmetic. For X=2 ={0, 1}we identify functions in 2Nwith points in the Cantor space, and for X=Nwe identify functions in NNwith points in the Baire space. Finite sequences of natural numbers can be encoded as a single natural number and this coding can be developed formally within RCA0. The set of all (codes of) finite sequences from Xis denoted X<N. The empty sequence is denoted . Given any s, t ∈X<N, |s|denotes the length of s, s(i) denotes the (i + 1)-th element of sfor i <|s|, and, for each n ≤|s|, s [n]is the n-th initial segment of s, i.e. s(0), ..., s(n−1). If s =t[n]for some n ≤|t|, we write s ⊆tand say that sis an initial segment of t(or tan extension of s). The concatenation of sand t, written s ∗t, is the sequence s(0), ..., s(|s|−1),t(0), ..., t(|t|−1). If f∈XN, s ∗fdenotes s(0), ..., s(|s|−1),f(0),f(1), ..., f(n), ..., and f[n] denotes f(0), ..., f(n−1). If s =f[|s|], we write s ⊂fand say that sis an initial segment of f(or fis an extension of s). Note that the relations s =, |s|=n, s(i) =n, s ⊆t, s =t ∗u, s =t [n], ...are formally defined as Σ0 0formulas in RCA0. 5 A formalization of classical two-person infinite games within second order arithmetic is described in section V.8 of [12]as well as in section 3 of [10]. To fix notation and terminology, we recall some basic notions. Our starting point is a given formula ϕ(f)with a distinguished function variable f∈XNand possibly other first and second order parameters. The language of second order arithmetic does not formally contain any function variables but one can naturally express the fact that “fis a function from Nto X” by using a Π0 2formula. (The price to pay is a possible increase of the quantifier complexity of the formulas involved. However, this is unimportant when working in the Cantor space, i.e. X={0, 1}, because in this case one can regard fas a set variable by identifying f(n) =0and f(n) =1with n /∈fand n ∈f, respectively.) An infinite game with pay-off set ϕ(f), denoted GX(ϕ), is defined as follows: Two players, say player I (male) and player II (female), alternately choose an element xin Xto form f∈XNwhich is called the resulting play. Player I plays first. Player I wins if and only if ϕ(f)holds. Otherwise Player II wins that play. If we define SeqX even ={s ∈X<N:|s|is even}and SeqX odd ={s ∈X<N:|s|is odd}, then a strategy for player I in the game GX(ϕ)is a function σI:Seq X even →Xand a strategy for player II in GX(ϕ)is a function σII :Seq X odd →X. If players I and II follow strategies σIand σII, respectively, the resulting play is uniquely determined and denoted by σI⊗σII. In fact, σI⊗σII is the function h :N→Xdefined by the recursive equations h(2k) =σI(h[2k]) and h(2k+1) =σII(h[2k+1]). A strategy for a player is a winning strategy if the player wins the game as long as he/she plays following it, no matter what his/her opponent plays. A game GX(ϕ)is determined if either player I or player II has a winning strategy: DetX(ϕ)≡∃σI∀σII ϕ(σI⊗σII)∨∃σII ∀σI¬ϕ(σI⊗σII), where σIand σII range over strategies for players I and II, respectively. Given a prescribed formula class Γ, Γ-determinacy axiom schemes declare that all games of pay-off set in Γare determined. Thus, •The scheme of Γ-determinacy in the Baire space, denoted Γ-Det, consists of all axioms DetN(ϕ), where ϕ(f)is in Γ. •The scheme of Γ-determinacy in the Cantor space, denoted Γ-Det∗, consists of all axioms Det{0,1}(ϕ), where ϕ(f)is in Γ. We are now in a position to describe a detailed formalization of Lipschitz and Wadge games in second order arithmetic as well as to introduce the Lipschitz and Wadge determinacy axiom schemes we will be interested in. 2.1. Formalized Lipschitz games Fix X⊆Nnonempty and consider formulas A(f)and B(g)with distinguished function variables f, g∈ XN. A Lipschitz game in the space XN, denoted GX L(A, B), is defined as follows: Two players, say player I (male) and player II (female), alternately choose an element xin Xto form the resulting plays f= x0, x1, x2, ... ∈XNand g=y0, y1, y2, ... ∈XN, respectively. Player I x0x1x2... Player II y0y1y2... Player I wins if and only if ¬(A(f) ↔B(g)) holds. Player II wins if and only if (A(f) ↔B(g)) holds. A strategy for player I in the game GX L(A, B)is a function σI:Seq X even →Xand a strategy for player II in the game GX L(A, B)is a function σII :Seq X odd →X. If players I and II follow strategies σIand σII, respectively, the resulting plays are uniquely determined. We will write σI⊗I LσII to denote player I’s resulting play and write σI⊗II LσII to denote player II’s resulting play. Note that σI⊗I LσII(n) =σI⊗σII(2n)and σI⊗II LσII(n) =σI⊗σII(2n +1). 6 The following axiom, denoted DetX L(A, B), expresses that the Lipschitz game GX L(A, B)is determined: ∃σI∀σII ¬(A(σI⊗I LσII)↔B(σI⊗II LσII)) ∨∃σII ∀σI(A(σI⊗I LσII)↔B(σI⊗II LσII)), where σIand σII range over strategies for players I and II, respectively. Definition 2.1. Fix X={0, 1}or N. Let Γ1and Γ2be classes of formulas with distinguished function variables f, g∈XN, respectively. 1. The scheme of (Γ1, Γ2)-Lipschitz determinacy in XN, denoted (Γ1, Γ2)-DetX L, is given by the axioms DetX L(A, B), where A(f)is in Γ1and B(g)is in Γ2. For simplicity, if Γ1=Γ 2=Γ, we will write Γ-DetX L instead of (Γ, Γ)-DetX L. 2. The scheme of (Δ0 n, Δ0 m)-Lipschitz determinacy in XN, denoted (Δ0 n, Δ0 m)-DetX L, is given by the axioms ∀f∈XN(A(f)↔C(f)) ∧∀g∈XN(B(g)↔D(g))→DetX L(A, B) where A(f)is in Σ0 n, C(f)is in Π0 n, B(g)is in Σ0 mand D(g)is in Π0 m. For simplicity, if n =m, we will write Δ0 n-DetX Linstead of (Δ0 n, Δ0 n)-DetX L. The schemes (Γ, Δ0 n)-DetX Land (Δ0 n, Γ)-DetX Lare defined similarly. We will omit the superscript Nfor determinacy schemes in the Baire space and write simply (Γ1, Γ2)-DetL, Δ0 n-DetL, etc.; whereas following [10], we will replace the superscript {0, 1}with ∗and write (Γ1, Γ2)-Det∗ L, Δ0 n-Det∗ L, ...to denote the corresponding determinacy schemes in the Cantor space. 2.2. Formalized Wadge games Fix X⊆Nnonempty and consider formulas A(f)and B(g)with distinguished function variables f, g∈ XN. A Wadge game in the space XN, denoted GX W(A, B), is defined as follows: Two players, say player I (male) and player II (female), alternately choose an element xin Xto form the resulting plays f= x0, x1, x2, ... ∈XNand g=y0, y1, y2, ... ∈XN, respectively. Player I plays first and in each of his turns he must choose an element xin X. In each of her turns, player II either chooses an element xin Xor has the option to pass but she has to play infinitely often otherwise she loses (below p denotes that player II passes): Player I x0x1x2x3... Player II y0ppy1... Player I wins if player II does not play infinitely often or ¬(A(f) ↔B(g)) holds. Player II wins if she plays infinitely often and (A(f) ↔B(g)) holds. When codifying a run of the play, for player II we will identify picking the number zero with passing and picking the number x +1with choosing x ∈Xto form her resulting play. As a consequence, player II will actually play in the set X+={0} ∪{i +1 :i ∈X}. As for player I, we opt for allowing him to play in set X+too and we will identify picking x ∈X+with choosing x ˙ −1 ∈Xto form his resulting play (where ˙ − denotes the modified subtraction function given by a ˙ −b =max(0, a −b)). As an example, a run of a Wadge game codified by 2, 2, 0, 0, 1, 1, 2, 0, ... will correspond to Player I 1001... Player II 1p0p... 7 Note that the code of a run of the play is not unique since for player I, choosing 0 to form his resulting play can be codified by using either 0 or 1. (For example, 2, 2, 1, 0, 0, 1, 2, 0, ... would be a different code of the previous run.) The following bounded formula θ(s, t) expresses that the finite sequences sand tare two codes of the same partial run of a Wadge game: |s|=|t|∧∀i<|s|(2i<|s|→s(2i)˙ −1=t(2i)˙ −1) ∧∀i<|s|(2i+1 <|s|→s(2i+1) = t(2i+1)). A strategy for player I in the game GX W(A, B) will be a function σI:Seq X+ even →X+, and a strategy for player II will be a function σII :Seq X+ odd →X+. But now we must require strategies to be coherent, in the sense that the output of the strategy does not depend on the particular code of a run of the play, that is: ∀s, t ∈SeqX+ even (θ(s, t) →σI(s) =σI(t)) and ∀s, t ∈SeqX+ odd (θ(s, t) →σII(s) =σII(t)). From now on, we assume that for Wadge games ‘strategy’ means ‘coherent strategy.’ Given strategies σIand σII, the restriction that player II must play infinitely often can be expressed by the Π0 2formula Inf(σI,σ II)≡∀n∃k>n((σI⊗σII)(2k+1)=0). If players I and II follow strategies σIand σII, respectively, and Inf(σI, σII)holds, the resulting plays are uniquely determined. We will write σI⊗I WσII to denote player I’s resulting play and write σI⊗II WσII to denote player II’s resulting play. Note that both σI⊗I WσII and σI⊗II WσII will be functions from Ninto X. Actually, we have σI⊗I WσII(n) =(σI⊗σII(2n)) ˙ −1and σI⊗II WσII(n) =(σI⊗σII(2 ·move(n) +1)) −1, where move(0) = μi [(σI⊗σII)(2i+1)=0] move(n+1)=μi [i>move(n)∧(σI⊗σII)(2i+1)=0]. The following axiom, denoted DetX W(A, B), expresses that the Wadge game GX W(A, B)is determined: ∃σI∀σII Inf(σI,σ II)→¬(A(σI⊗I WσII)↔B(σI⊗II WσII)) ∨∃σII ∀σIInf(σI,σ II)∧(A(σI⊗I WσII)↔B(σI⊗II WσII)), where σIand σII range over strategies for players I and II, respectively. Definition 2.2. Fix X={0, 1}or N. Let Γ1and Γ2be classes of formulas with distinguished function variables f, g∈XN, respectively. 1. The scheme of (Γ1, Γ2) Wadge determinacy in XN, denoted (Γ1, Γ2)-DetX W, is given by the axiom scheme DetX W(A, B) where A(f)is in Γ1and B(g)is in Γ2(if Γ1=Γ 2=Γ, we will simply write Γ-DetX W). 2. Likewise (Δ0 n, Δ0 m)-DetX W, (Γ, Δ0 n)-DetX Wand (Δ0 n, Γ)-DetX Ware defined as in Definition 2.1. Also, we will omit the superscript Nfor determinacy schemes in the Baire space and replace the superscript {0, 1}with ∗for determinacy schemes in the Cantor space. Remark 2.3. It is easily verified that Γ-DetXand (¬Γ)-DetXare equivalent principles over RCA0. A similar result holds for Lipschitz and Wadge determinacy: (Γ1, Γ2)-DetX L/W and (¬Γ1, ¬Γ2)-DetX L/W are equivalent over RCA0and in this case the proof is trivial, because GX L/W (A, B)and GX L/W (¬A, ¬B)are essentially the same game. Remark 2.4. Lipschitz and Wadge games can be naturally reduced to classical infinite games. This reduction is effective and checkable in RCA0. However, there is a price to pay: a possible increase of the pay-off set complexity. Fix X⊆Nnonempty and consider formulas A(f), B(g)with f, g∈XN. Let us start by 8 analysing the Lipschitz case. The resulting plays in a Lipschitz game f=hI, g=hII can be defined by composition from the resulting play in a classical infinite game h. In fact, hI(n) =h(2n)and hII(n) = h(2n +1). Put TransL(A, B)(h)≡¬(A(hI)↔B(hII)), where hranges over functions in XN. It is easy to check that DetX(TransL(A, B)) →DetX L(A, B). Since ¬(A(hI) ↔B(hII)) is equivalent to (A(hI) ∨B(hII)) ∧(¬A(hI) ∨¬B(hII)), this reduction allows one to infer Lipschitz Γ-determinacy from determinacy for Γ ∧¬Γsets (We are assuming that Γis closed under conjunction and disjunctions.) This provides us with a first upper bound on the strength of Lipschitz Γ-determinacy. This upper bound needn’t be, however, sharp. Consider, for example, Γ =Σ 0 4. By a result of Louveau and Saint-Raymond [6] second order arithmetic proves Σ0 4-DetL, whereas by a result of Martin [7]second order arithmetic does not prove Σ0 4∧Π0 4-Det. It should be noted that in [9]Nemoto studied the logical strength of several axiom schemes formalizing the determinacy of classical infinite games whose pay-off sets are of the form Sep(Γ1, Γ2) ={(A ∧¬B) ∨(¬A ∧C) : A ∈Γ1, B, C∈Γ2}. Since ¬(A(hI) ↔B(hII)) is equivalent to (A(hI) ∧¬B(hII)) ∨(¬A(hI) ∧B(hII)), a Lipschitz game whose pay-off sets have complexity (Γ1, Γ2) unravels to an infinite game of complexity Sep(Γ1, Γ2). Thus, using the results in [9], one can obtain upper bounds on the strength of Lipschitz (Γ1, Γ2)-determinacy. Again, these upper bounds needn’t be sharp, for the translations of (Γ1, Γ2)Lipschitz games give rise to special cases of Sep(Γ1, Γ2) games. As to the Wadge case, we have to modify the way we recover the resulting plays because now player II is allowed to pass. To this end, given h ∈(X+)Nput hI,W (n) =h(2n)˙ −1and hII,W (n) =h(2 ·move(h)(n) + 1)) −1, where move(h)is given by the recursive equations move(h)(0) = μi [h(2i+1)=0], move(h)(n+1)=μi [i>move(h)(n)∧h(2i+1)=0]. Let Inf(h)denote the Π0 2formula ∀n ∃k(k>n ∧h(2k+1) = 0) expressing that player II plays infinitely often and put TransW(A, B)(h)≡Inf(h)→¬(A(hI,W )) ↔B(hII,W )). It is easy to see that DetX+(TransW(A, B)) →DetX W(A, B). Roughly speaking, the previous reduction allows one to infer Wadge Γ-determinacy from determinacy for max(Σ0 2, Γ ∧¬Γ) sets. The possible increase of the pay-off set complexity is now much worse due to the presence of the Π0 2formula Inf(h)in the translation of the game. For example, the translation of a clopen Wadge game would already give rise to a Σ0 2classical game. 3. Determinacy for clopen sets In [16] Wadge developed a careful level-by-level analysis of the structure of Wadge degrees (i.e. equivalence classes relative to ≤W) in the Baire space below Δ0 2. In this and the following section, we will show that this topological analysis can be adapted to prove Lipschitz and Wadge determinacy for the first levels of the Hausdorff difference hierarchy in the Cantor space. In the present section we will deal with clopen determinacy. Our starting point is the standard representation of closed sets of the Cantor space as sets of paths of binary trees. A set T⊆X<Nis called a tree over Xif Tis closed under initial segments, i.e. s ∈Tand t ⊆simply t ∈T. We call the elements of Tthe nodes of T. A tree is infinite if, for any n, there exists s ∈Twith 9 |s|=n, i.e. if the set of nodes of Tis infinite. If S⊆X<Nis a tree over Xand S⊆T, then Sis called a subtree of T. Fix any tree T⊆X<N. A node s ∈Tis called terminal if it has no proper extension in T, i.e. if ∀a ∈X(s∗a/∈T). A function f∈XNis called a path of Tif ∀n ∈N(f[n]∈T). The body of Tis written as [T]and is the set of all paths of T, i.e. [T]={f∈XN:∀n∈Nf[n]∈T}. Proposition 3.1 ([12], Lemma VI.1.5). For each formula ϕ(f) ∈Π0 1, RCA0proves that there is a tree T⊆X<Nsatisfying that [T] ={f∈XN:ϕ(f)}. By abuse of language, we will use set theoretic notations to mean the arithmetic formula expressing the corresponding set. For instance, an expression of the form f∈[T] denotes the Π0 1formula ∀n (f[n] ∈T) expressing that fis a path of Tand, accordingly, an expression of the form f∈[T] −[S]is to be understood as the Π0 1∧Σ0 1formula expressing that fis a path of Tand is not a path of S. Definition 3.2. Fix X⊆Nnonempty and consider a tree T⊆X<N. We say that Tdefines a clopen set if there exists another tree T⊆X<Nsuch that ∀f∈XN(f/∈[T] ↔f∈[T]). We say that Tproperly defines a finitely decidable set if ∃k∀f∈XN(f∈[T] ↔f[k] ∈T). It is easily proved in RCA0that if Tis a binary tree that properly defines a finitely decidable set then T defines a clopen set. The converse can be proved in WKL0and, so, over WKL0both notions are equivalent. Even more, we have Lemma 3.3. Over RCA0, WKL0is equivalent to the assertion “every binary tree defining a clopen set properly defines a finitely decidable set.” Proof. First, let us reason in WKL0and consider binary trees Tand Tsuch that ∀f∈XN(f/∈[T] ↔f∈ [T]). Clearly, T∩Tis a binary tree with no path. By WKL0, T∩Tmust be finite. Pick k∈Nsuch that all sequences in T∩Thave length at most k. Then, ∀f∈XN(f∈[T] ↔f[k+1] ∈T). Second, reason in RCA0and assume WKL0fails. Let T1be an infinite binary tree with no path. Then, it is easy to see that T1defines a clopen set but T1does not properly define a finitely decidable set.  Definition 3.4. A tree T⊆X<Nis said to be pruned if every sequence of Tlies on a path of T, i.e. ∀s ∈X<N(s ∈T→∃f∈XN(s ⊂f∧f∈[T])). It is well known that the assertion that every tree T⊆N<Ncan be pruned (that is to say, for every tree there exists some pruned subtree with the same set of paths) is equivalent over RCA0to Π1 1-CA0(see, e.g., Lemma VI.4.4 of [12]). Here we show that if we restrict ourselves to binary trees then we can prune a tree at a lower price. We first need the following lemma asserting that Π0 1formulas are closed in WKL0under existential quantifiers of the form ∃f∈2N. Lemma 3.5 (see [12], Lemma VIII.2.4, or [10], Lemma 3.2). Let ψbe a Π0 1formula. Within WKL0, ∃f∈ 2Nψ(f)is equivalent to a Π0 1formula. Lemma 3.6. 1. Let ϕ(f) ∈Π0 1. ACA0proves that there is a pruned binary tree Tsuch that [T] ={f∈2N:ϕ(f)}. 16 By Δ0 0-induction we get ∀i (h(i) ∈S0)and therefore f(i) =(h(i + 1))(i) defines a path of T0, which gives us a contradiction. As a consequence, player II cannot have a winning strategy either and, thus, the game GL([T1], [T2]) would not be determined contradicting Δ0 1-Det∗ L. In the next section we show that ACA0proves open (or closed) Lipschitz determinacy in the Cantor space. However, we close this section by showing that WKL0is still sufficient when one player plays in an open or closed set and her/his opponent plays in a clopen one (we will make use of this result in the proofs of Theorems 4.4 and 4.8). Proposition 3.12. WKL0proves (Δ0 1, Σ0 1)-Det∗ Land (Σ0 1, Δ0 1)-Det∗ L. Proof. We work in an arbitrary model of WKL0. We will prove (Δ0 1, Π0 1)-Det∗ L, which is equivalent to (Δ0 1, Σ0 1)-Det∗ L. (The proof for (Σ0 1, Δ0 1)-Det∗ Lis similar and we omit it.) Consider A(f) ∈Σ0 1, A(f) ∈Π0 1and B(g) ∈Π0 1such that ∀f∈2N(A(f) ↔A(f)). We may safely assume that neither A(f)nor B(g) defines the empty set or the total set. By Proposition 3.1, there is a binary tree Tsuch that [T] ={g∈2N:B(g)}and, by Lemma 3.6, there are nonempty pruned binary trees S, Ssuch that [S] ={f∈2N:A(f)}and [S] = {f∈2N:¬A(f)}. As in Lemma 3.8, we consider hS=max{|s| :s ∈S∩S}. Define X=Xin ∩Xout where Xin ={t∈2<N:|t|=hS∧t∈T∧∃g∈2N(t⊂g∧g∈[T])},and Xout ={t∈2<N:|t|=hS∧t∈T∧∃t(t⊆t∧t/∈T)} The existence of such sets follows by bounded Σ0 1or bounded Π0 1comprehension (which are well known to be provable from RCA0) and by the fact that Π0 1formulas are closed in WKL0under quantifiers of the form ∃g∈2N(see Lemma 3.5). Intuitively, Xcomprises those positions of length hSfor which player II still has the possibility of playing inside or outside the closed set [T]. Case 1: Xis nonempty. Then player II has a winning strategy. Namely, we define σII as follows. Pick t0∈Xand gin ,g out ∈ 2Nsuch that t0⊂gin, t0⊂gout, gin ∈[T]and gout /∈[T]. Given any sequence of odd length, s = x0, y0, ..., xn−1, yn−1, xn, we define σII(s)=⎧ ⎪ ⎨ ⎪ ⎩ t0(n)ifn<h S gin(n)ifn≥hSand x0,...,x hS∈S gout(n)ifn≥hSand x0,...,x hS/∈S It is clear that σII exists by Δ0 1comprehension and in view of the properties of hSin Lemma 3.8, it is immediate to see that σII is winning for player II. Case 2: Xis empty. Then player I has a winning strategy. On the one hand, since X=∅, we have ¬∃t (t ∈Xin ∧t ∈Xout)and thus ∀t(t∈Xin →∀g∈2N(t⊂g→g∈[T])) and ∀t(t∈Xout →∀g∈2N(t⊂g→g/∈[T])). On the other hand, picking s0∈S∩Swith |s0| =hS, it follows from Lemma 3.8, that there are fin ,f out ∈ 2Nsuch that s0⊂fin, s0⊂fout, fin ∈[S]and fout /∈[S]. Having these facts in mind, given any sequence of even length, s =x0, y0, ..., xn−1, yn−1, we define 17 σI(s)=⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ s0(n)ifn<h S fin(n)ifn≥hSand y0,...,y hS−1/∈T fout(n)ifn≥hSand y0,...,y hS−1∈Xin fin(n)ifn≥hSand y0,...,y hS−1∈Xout Again, σIexists by Δ0 1comprehension and it is easy to see that σIis winning for player I.  Let us observe that an alternative proof of Proposition 3.12 can be obtained by putting together Theorem 3.7 of [9]and the fact that a (Δ0 1, Σ0 1)Lipschitz game can be reduced to a Bisep(Δ0 1, Σ0 1) infinite game, as defined in [9]. Also, note that in [4]it is proved that Proposition 3.12 can be extended a bit further: (Σ0 1∧Π0 1, Δ0 1)-Det∗ Lis still provable within WKL0(although we will not make use of this extended result in the present paper). 4. Determinacy for open sets and differences of closed sets In the analysis of determinacy properties of a closed set [T], the structure of its topological boundary will be relevant. In the previous section we have dealt with the simpler case where [T]is a clopen set and, therefore, its boundary is empty. However, in cases where [T]is not clopen ([T]is, so to say, a “true” closed set) it must have some boundary points. The following definition isolates this notion. Definition 4.1. We say that a binary tree Tdefines a true closed set if TrueClosed(T)≡∃f∈2N[f∈[T]∧∀k∃s(f[k]⊆s∧s/∈T)]. It is a well-known fact from general topology that a set is clopen if and only if its boundary is empty. Hence a basic dichotomy concerning closed sets emerges: either they are clopen or they must have some boundary points. ACA0is strong enough to show this fact: Lemma 4.2. ACA0proves that if Tis a binary tree that does not define a clopen set then TrueClosed(T). Proof. Suppose that Tis a binary tree that does not define a clopen set. Then, Tdoes not properly define a finitely decidable set either and we have ∀k∃f∈2N(f[k] ∈T∧f/∈[T]) and so ∀k∃s, t ∈2<N(|s|=k∧s⊂t∧s∈T∧t/∈T). (†) Define Tto be {s ∈2<N:s ∈T∧∃t (s ⊂t ∧t /∈T)}. Note that Texists by Σ0 1comprehension (which is available thanks to ACA0). Clearly, Tis a binary tree and it follows by (†)that Tis infinite. By applying Weak König Lemma we obtain that Thas a path, say g∈2N. Since T⊆T, g∈[T]. In addition, by the definition of Twe have ∀k∃s (g[k] ⊂s ∧s /∈T). Thus, we have shown that TrueClosed(T)holds, as required.  Note that in the proof of Lemma 4.2 we have indeed shown the following dichotomy property to hold: Definition 4.3. Let (DP)denote the formula ∀T(BinaryTree(T)→TrueClosed(T)∨Tproperly defines a finitely decidable set), where BinaryTree(T)is a formula declaring that Tis a binary tree. 18 We shall use (DP)as a basic principle to be added to RCA0in order to derive Σ0 1-determinacy. Theorem 4.4. The following principles are provable in RCA0+(DP): 1. Σ0 1-Det∗ L. 2. Σ0 1-Det∗ W. Proof. Firstly, let us note that RCA0+(DP) extends WKL0. Indeed, if Tis an infinite binary tree and TrueClosed(T)h olds then, by definition, Thas a path. If TrueClosed(T)does not hold, by (DP) there is some ksuch that for all f∈2N, f∈[T] ↔f[k] ∈T. Since Tis infinite, there exists s ∈Twith |s| >kand we define g∈2Nby putting g(j) =s(j), for j<|s|, and g(j) =0for j≥|s|. It is clear that g∈[T], as required. Hence, we work in an arbitrary model of WKL0+(DP). (1)W e will prove Π0 1-Det∗ L, which is equivalent to Σ0 1-Det∗ L. Consider A(f), B(g) ∈Π0 1. By Proposition 3.1 there are binary trees Sand Tsatisfying that [S] ={f∈2N:A(f)}and [T] ={g∈2N:B(g)}. We must show that the game GL([S], [T]) is determined. Case A: TrueClosed(T)holds. Then, player II has a winning strategy. Actually, pick g0∈2Nsatisfying that g0∈[T] ∧∀k∃t (g0[k] ⊂t ∧t /∈ T). Using RCA0, we get h :N→2<Nsuch that ∀k(g0[k] ⊂h(k) ∧h(k) /∈T). Define Hto be the set given by (k,n,i)∈H↔(n<|h(k)|∧i=h(n)) ∨(n≥|h(k)|∧i=0). Clearly, Hexists by Δ0 1comprehension. We will write Hk(n) =ifor (k, n, i) ∈H. Thus, each function Hk extends the finite sequence h(k)by putting zeros on the end. We are now in a position to define a strategy for player II, σII, as follows. Given any sequence of odd length s =x0, y0, ..., xn−1, yn−1, xn, we define σII(s)=g0(n)ifx0,...,x n∈S Hk(n)ifx0,...,x n/∈Sand k=μj (x0,...,x j/∈S) (In words, player II plays using the boundary point g0while player I has played inside Sand if player I leaves Sat round kthen player II will also leave Tby using h(k).) Again, σII exists by Δ0 1comprehension and it is straightforward to see that σII is winning for player II. Case B: TrueClosed(T)does not hold. By (DP) there exists some k0∈Nsatisfying that ∀g∈2N(g∈[T] ↔g[k0] ∈T). Let B(g)be the Σ0 1-formula g[k0] ∈T. Then, ∀g∈2N(B(g) ↔B(g)) and so GL([S], [T]) is determined by Proposition 3.12. (2)We will prove again Π0 1-Det W. Consider A(f), B(g) ∈Π0 1. By Proposition 3.1 there are binary trees S and Tsatisfying that [S] ={f∈2N:A(f)}and [T] ={g∈2N:B(g)}. We must show that the game GW([S], [T]) is determined. The proof is similar to that of the Lipschitz case. Since a winning strategy for player II in GL([S], [T]) immediately gives rise to a winning strategy for player II in GW([S], [T]), the only situation that deserves some explanations is case B above. Thus, assume that TrueClosed(T)does not hold. If TrueClosed(S)does not hold either, by (DP)both Tand Sdefine a clopen set and GW([S], [T]) is determined by Theorem 3.9. So, let us assume that TrueClosed(S)holds. On the one hand, there exists f0∈2Nsuch that f0∈[S] ∧∀k∃s (f0[k] ⊆s ∧s /∈S) and, on the other hand, by (DP) there exists some k0∈Nsuch that ∀g∈2N(g∈[T] ↔g[k0] ∈T). Using RCA0, we get h :N→2<Nsatisfying that ∀k(f0[k] ⊆h(k) ∧h(k) /∈S). As in the proof of Case A of part (1), there exists a sequence of functions, {Hk:k∈N}, such that each Hkextends the finite sequence h(k)by putting zeros on the end. Since now player II is allowed to pass, we also need a function ext :2 <N→2<Nsuch 19 that ext(s)is the finite sequence obtained by dropping the zeros of the finite sequence sand decreasing the values by 1. (Recall that in coding a strategy for a Wadge game, for player II we identify passing with picking the number 0 and for both players we identify playing iwith picking i +1.) We are now in a position to define a winning strategy for player I. Given any sequence of even length, s =x0, y0, ..., xn−1, yn−1, we put σI(s)=⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ f0(n)+1 if|ext (y0,...,y n−1)|<k 0 Hk(n)+1 if |ext (y0,...,y n−1)|≥k0and ext (y0,...,y n−1)[k0]∈T and k=μj (|ext (y0,...,y j−1)|≥k0) f0(n)+1 if|ext (y0,...,y n−1)|≥k0and ext (y0,...,y n−1)[k0]/∈T (In words, player I plays using the boundary point f0until player II has played (not passed) k0times. At that round player II has already decided whether or not she will play inside Tand player II will play accordingly.) Then, σIexists by Δ0 1comprehension and it is easy to verify that σIis winning for player I. This completes the proof of the theorem.  Corollary 4.5. Σ0 1-Det∗ Land Σ0 1-Det∗ Ware provable in ACA0. Proof. It follows from Lemma 4.2 and Theorem 4.4. Remark 4.6. The fact that ACA0proves Σ0 1-Det∗ Lcan also be derived from known results on determinacy of infinite games. On the one hand, in [10] Nemoto, MedSalem and Tanaka showed that ACA0proves general determinacy for the second level of the difference hierarchy (Σ0 1)2(where (Σ0 1)2coincides with Σ0 1∧Π0 1). On the other hand, we showed in Remark 2.4 that an open Lipschitz game can be reduced to a infinite game of pay-off set complexity Σ0 1∧Π0 1. In the next result we calibrate the exact strength of the principle (DP)over RCA0. The basic ideas in the proof were suggested to us by Paul Shafer. As a matter of fact, he has proved a stronger version of this result.1 Theorem 4.7. The following principles are equivalent over RCA0: 1. ACA0. 2. (DP). 3. Each infinite binary tree has a leftmost path. That is, for every infinite binary tree Tthere is f∈[T] such that for any other path g∈[T], there exists k∈Nsuch that f[k] =g[k]and f(k) <g(k). Proof. (1) ⇒(2) follows by Lemma 4.2. (2) ⇒(3): We work in WKL0+(DP) (recall that in the proof of Theorem 4.4 we showed that RCA0+(DP) extends WKL0.) Let Tbe an infinite binary tree. We shall prove that Thas a leftmost path. To this end, let T∗be the set of binary finite sequences defined by s∈T∗⇐⇒ ⎧ ⎪ ⎨ ⎪ ⎩ s∈T∨ ∃s0∃ts=s0∗t∧s0∈T∧s0∗t(0)/∈T∧ ∃s1∈T(|s1|=|s|∧left(s1,s 0)) 1Paul Shafer has proved ([11], personal communication) that ACA0can be already derived over RCA0from the principle: “Every closed and not open set in the Cantor space has a boundary point.” 20 where left(s1, s0) expresses that s1is to the left of s0. Namely, s1⊆s0∨∃j<|s1|(s1[j]=s0[j]∧s1(j)<s 0(j)). Likewise, for f, g∈2Nwe say that fis to the left of gif ∃j(f[j] =g[j] ∧f(j) <g(j)). It can be easily checked, by using Δ0 1-comprehension, that T∗does exist and that it is a tree. The following facts easily follow from the definition of T∗: (†)Suppose g∈[T∗]. If g/∈[T]then there is f∈[T]such that fis to the left of g. Proof. If g/∈[T]then there exists l∈Nsuch that g[l+1] /∈T∧g[l] ∈T. For each m >l, since g[m] ∈T∗−T, it follows from the definition of T∗that there is sm∈Tsatisfying left(sm, g[l]) and |sm| =|g[m]| =m. As a consequence, we get an infinite tree Tl,g ={s ∈T:|s| ≤l∨left(s, g[l])}. By WKL0, there exists f∈[Tl,g] ⊆[T]and it is obvious that fis to the left of g. (‡) Suppose g∈[T∗]. If there is f∈[T]such that fis to the left of g, then gis an interior point of [T∗] (that is to say, ∃k∀s ∈2<N(g[k] ⊆s →s ∈T∗).) Proof. Let f∈[T]be such that for some k, f[k] =g[k]and f(k) <g(k). For all m >k, we have f[m]∈T∧left(f[m],g[k+1]). It is easy to see that for all w∈2<N, s =g[k+1] ∗w∈T∗. To check this, observe that if s /∈Tthen there is l≥ksuch that s[l] ∈Tand s[l] ∗s(l) /∈T. Therefore, taking s0=s[l]and t ∈2<Nsuch that s =s0∗t, we get that left(f[|s|], s0)holds (note that f[k] ⊆s0and f(k) <s(k)) and so s ∈T∗. Since T⊆T∗, T∗is infinite, and by (DP)either T∗properly defines a finitely decidable set or TrueClosed(T∗) holds. We distinguish these two cases. Case 1: T∗properly defines a finitely decidable set. By Lemma 3.6 we can assume without loss of generality that T∗is a pruned tree. Let g∈[T∗] defined by g(n)=min{j∈{0,1}:g[n]∗j∈T∗}. Clearly, gis the leftmost path of T∗. By (†), g∈[T] and, since [T] ⊆[T∗], gis also the leftmost path of [T]. Case 2: TrueClosed(T∗)holds. Then there exists g∈[T∗]such ∀j∃s (g[j] ⊆s ∧s /∈T∗). Observe that by (†), if g/∈[T]then there is f∈[T]such that fis to the left of g. But then by (‡), gwould be an interior point of [T∗], contradicting our hypothesis on g. Thus, g∈[T]. As a consequence, gis the leftmost path of T(for otherwise again by (‡), gwould be an interior point of [T∗].) (3) ⇒(1): See [3], Lemma 3.1.  Using the same ideas as in the proof of Theorem 4.4, we can derive a slightly sharper version of Corollary 4.5, which will be useful in section 5to characterize ACA0in terms of the Semi-Linear Ordering Principle SLO. Theorem 4.8. (1) ACA0proves (Σ0 1, Σ0 1∧Π0 1)-Det∗ L. (2) ACA0proves (Σ0 1, Σ0 1∧Π0 1)-Det∗ W. 21 Proof. We work in an arbitrary model of ACA0. (1) Consider A(f) ∈Σ0 1and B(g) ∈Σ0 1∧Π0 1. We must show that GL(A, B)is determined. By Lemma 3.6, there exist binary pruned trees S, T0and T1such that T1⊆T0and A(f)↔f/∈[S],and B(g)↔g∈[T0]−[T1]. Put T2={t ∈T1:∃t(t∈T0−T1∧t ⊆t)}. Clearly, T2is a subtree of T1and T2exists by Σ0 1-comprehension. Case A: [T2] =∅. Then, player II has a winning strategy in the game GL(A, B). Actually, pick g0∈[T2]. Then g0satisfies that g0∈[T1]∧∀k∃t∈T0(g0[k]⊂t∧t/∈T1)]. By Δ0 1comprehension, there exists h :N→T0satisfying that ∀k(g0[k] ⊂h(k) ∧h(k) ∈T0∧h(k) /∈T1). Define H:N2→Nto be the function defined by recursion as follows: H(k,n)=⎧ ⎪ ⎨ ⎪ ⎩ g0(n)ifn<k h(k)(n)ifk≤n<|h(k)| min{j≤1: H(k,0),...,H(k,n −1),j∈T0}otherwise Since T0is a pruned tree, His well defined and, writing Hk(n) =H(k, n), each function Hkextends the finite sequence h(k)to a path through [T0]. We are now in a position to define a strategy for player II, σII, as follows. Given any sequence of odd length s =x0, y0, ..., xn−1, yn−1, xn, we define σII(s)=g0(n)ifx0,x 1,...,x n∈S Hk(n)ifx0,x 1,...,x n/∈Sand k=min{j:x0,x 1,...,x j/∈S} Again, σII exists by Δ0 1comprehension and it is straightforward to see that σII is winning for player II. Case B: [T2] =∅. By WKL0, T2must be finite. Pick k0∈Nsuch that all sequences in T2have length below k0. Consequently, we obtain that ∀g∈2N(B(g)↔g∈[T0]∧g[k0]/∈T1) and hence B(g)is equivalent to a Π0 1-formula. Let Tbe a binary pruned tree such that [T] ={g∈2N: B(g)}. We must show that GL(A, [T]) is determined. We distinguish two cases. Case B.1: TrueClosed(S)holds. Then, player I has a winning strategy. To see this, pick f0∈[S]such that ∀k∃s (f0[k] ⊆s ∧s /∈S). By Δ0 1 comprehension, there exists h :N→2<Nsuch that ∀k(f0[k] ⊆h(k) ∧h(k) /∈S)and so we have ¬A(f0)∧∀k∀f∈2N(h(k)⊂f→A(f)).(†) As in the previous case, consider a sequence of functions, {Hk:k∈N}, such that each function Hkextends the finite sequence h(k) but now by putting zeros on the end. We define a strategy for player I as follows. Given any sequence of even length s =x0, y0, ..., xn−1, yn−1, we put σI(s)=f0(n)ify0,...,y n−1∈T Hk(n)ify0,...,y n−1/∈Tand k=μj (y0,...,y j−1/∈T) 22 Note that σIexists by Δ0 1comprehension and it follows by (†)that σIis winning for player I. Case B.2: TrueClosed(S)does not hold. By (DP), there is k1∈Nsuch that ∀f∈2N(A(f) ↔f[k1] /∈S). Thus, the fact GL(A, [T]) is determined follows from (Δ0 1, Π0 1)-Det L(which is available in WKL0by Proposition 3.12). (2) The proof of part (1) can be easily adapted to provide a proof of (Σ0 1, Σ0 1∧Π0 1)-Det∗ W. We omit the details.  Remark 4.9. In [5], using similar but combinatorially more complex methods, it was showed that ACA0also proves (Σ0 1∧Π0 1)-Det∗ L. As a matter of fact a reversal for ACA0was derived by showing that, over RCA0, this determinacy principle is equivalent to ACA0. However, in the present article Theorem 4.8 suffices to obtain reversals for ACA0(see Theorems 5.5 and 5.7 below). 5. The semi-linear ordering principle In the setting of descriptive set theory and working in the Baire space, in [16] Wadge showed that the relations ≤L(reducibility via Lipschitz functions) and ≤W(reducibility via continuous functions) can be characterized in terms of infinite games. Wadge’s Lemma from [16] states that i) player II has a winning strategy in GL(A, B)(resp. GW(A, B)) iff A ≤LB(resp. A ≤WB); and ii) if player I has a winning strategy in GL(A, B)or GW(A, B)then Bc≤LA, where Xcdenotes the complement of the set X. The Axiom of Determinacy AD therefore implies the following comparability property (known as the Semi-Linear Ordering principle SLO): SLOW=“ForallA, B ⊆ωω,eitherA≤WBor Bc≤WA,” SLOL=“ForallA, B ⊆ωω,eitherA≤LBor Bc≤LA.” Wadge soon realized the relevance of SLO in order to establish the structure of the Lipschitz/Wadge degrees (i.e. the equivalence classes generated by the pre-orders ≤Land ≤W). He also showed that SLO shares important consequences with AD: SLOWproves the perfect set property (every subset of ωωis either countable or else it contains a copy of the Cantor set) and therefore SLOWis incompatible with the Axiom of Choice. In fact, some years later, A. Andretta (see [1]and [2]) was able to prove that, over certain settheoretic base theory, the principles ADW=“all Wadge games are determined,” ADL=“all Lipschitz games are determined,” SLOLand SLOWare pairwise equivalent. (Whether SLOWis also equivalent to the full Axiom of Determinacy AD under some appropriate set-theoretical assumptions is still an open question.) In this section we present a formalization of the semi-linear ordering principle within second order arithmetic and we initiate the study of the reverse mathematics of this principle. Our formalization is based on the aforementioned characterization of ≤Land ≤Win terms of Lipschitz/Wadge games. Fix X⊆N nonempty and consider formulas A(f)and B(g)with distinguished function variables f, g∈XN. We say that Ais Lipschitz reducible to Bif player II has a winning strategy in the Lipschitz game GX L(A, B): RedX L(A, B)≡∃σII ∀σI(A(σI⊗I LσII)↔B(σI⊗II LσII)), where σIand σII range over strategies for players I and II, respectively. In a similar vein, Ais Wadge reducible to Bif player II has a winning strategy in the Wadge game GX W(A, B): RedX W(A, B)≡∃σII ∀σI[Inf(σI,σ II)∧(A(σI⊗I WσII)↔B(σI⊗II WσII))]. Definition 5.1. Fix X={0, 1}or N. Let Γ1and Γ2be classes of formulas with distinguished function variables f, g∈XN, respectively. 23 1. The scheme of (Γ1, Γ2)Lipschitz semi-linear ordering principle in XN, denoted (Γ1, Γ2)-SLOX L, is given by the axiom scheme RedX L(A, B) ∨RedX L(¬B, A), where A(f)is in Γ1and B(g)is in Γ2. 2. The scheme of (Γ1, Γ2) Wadge semi-linear ordering principle in XN, denoted (Γ1, Γ2)-SLOX W, is given by the axiom scheme RedX W(A, B) ∨RedX W(¬B, A), where A(f)is in Γ1and B(g)is in Γ2. 3. (Δ0 n, Δ0 m)-SLOX L/W , (Γ, Δ0 n)-SLOX L/W and (Δ0 n, Γ)-SLOX L/W are defined similarly. Using our notation conventions, we will simply write Γ-SLOX L/W or Δ0 n-SLOX L/W when Γ1=Γ 2=Γor n =m. Also, we will omit the superscript Nfor schemes in the Baire space, and we replace {0, 1}with ∗ for schemes in the Cantor space. Next lemma states two basic properties of the semi-linear ordering principle: SLO can be inferred from determinacy, and SLOLimplies SLOW. Lemma 5.2. Fix X={0, 1}or N. It is provable over RCA0that 1. (Γ1, Γ2)-DetX L/W implies (Γ1, Γ2)-SLOX L/W , and the same holds for classes (Δ0 n, Δ0 m), (Γ, Δ0 m), (Δ0 n, Γ). 2. (Γ1, Γ2)-SLOX Limplies (Γ1, Γ2)-SLOX W, and the same holds for classes (Δ0 n, Δ0 m), (Γ, Δ0 m), (Δ0 n, Γ). Proof. (1): We only write the proof for the Lipschitz case, the Wadge case being analogous. Reasoning in RCA0, assume (Γ1, Γ2)-DetX L. Consider A(f) ∈Γ1and B(g) ∈Γ2. We must show that either RedX L(A, B) or RedX L(¬B, A)holds. By hypothesis, GX L(A, B)is determined. If player II has a winning strategy in that game then there is nothing to prove. So assume that player I has a winning strategy, i.e. there is σsuch that ∀σII ¬(A(σ⊗I LσII) ↔B(σ⊗II LσII)) holds. Define τto be the strategy for player II given by τ(x0)=σ(), τ(x0,y 0,...,x k,y k,x k+1)=σ(y0,x 0,...,y k,x k). It is easy to check that τis a winning strategy for player II in GX L(¬B, A), as required. (2): It suffices to note that a winning strategy for player II in GX L(A, B) automatically gives rise to a winning strategy for player II in the corresponding Wadge game GX W(A, B).  In view of Lemma 5.2 and our results on L/W-determinacy in the previous sections, we obtain that Corollary 5.3. 1. RCA0proves Δ0 1-SLO∗ W, (Δ0 1, Σ0 n)-SLO∗ Wand (Σ0 n, Δ0 1)-SLO∗ W, for every n >0. 2. WKL0proves Δ0 1-SLO∗ L, (Δ0 1, Σ0 1)-SLO∗ Land (Σ0 1, Δ0 1)-SLO∗ L. 3. ACA0proves Σ0 1-SLO∗ L/W and (Σ0 1, Σ0 1∧Π0 1)-SLO∗ L/W . Proof. Only the fact that RCA0implies (Σ0 n, Δ0 1)-SLO∗ Wis not a direct consequence of previously proved results for L/W-determinacy. Consider n >0, A(f) ∈Σ0 nand B(g) ∈Δ0 1. Then, ¬B(g)is also in Δ0 1and we get that RedX W(¬B, A)holds by reasoning as in part (2) of Proposition 3.9. The main results of the present section are two reversals for ACA0in terms of the semi-linear ordering principle SLO∗ W(Propositions 5.4 and 5.6 below). The interest of these results is, we think, twofold. First, since SLO∗ Wis the weakest one among the considered axiom schemes, obtaining reversals in terms of SLO∗ W makes our results stronger. Second, as a by-product we establish that, for Σ0 1and (Σ0 1, Σ0 1∧Π0 1)sets SLO∗ W is, after all, as strong as SLO∗ Land L/W-determinacy (a miniaturisation of the above mentioned Andretta’s result in Set Theory). 24 Proposition 5.4. Over WKL0, Σ0 1-SLO∗ Wimplies ACA0. Proof. By Theorem 4.7 it is sufficient to show that WKL0+¬(DP) implies that Π0 1-SLO∗ Wfails. Work in WKL0and assume ¬(DP). Then there is a binary tree Tsuch that Tdoes not properly define a finitely decidable set and TrueClosed(T)does not hold. Hence, we have i) ¬∃k∀f∈2N(f[k] ∈T→f∈[T]), and ii) ∀f∈2N(f∈[T] →∃k∀t (f[k] ⊆t →t ∈T)). Define A(f) ≡∀i (f(i) =0)and B(g) ≡g∈[T]. Note that A, B∈Π0 1. Claim 5.4.1. Player II cannot have a winning strategy in GW(A, B). Proof. Towards a contradiction, suppose σis a winning strategy for player II in that game. Consider the strategy for player I given by τ1(s) =0for all s ∈Seq{0,1,2} even (We will use the terminology and conventions for formalized Wadge games introduced in subsection 2.2.) Then we must have Inf(τ1, σ)and h =τ1⊗II Wσ∈[T]. By condition ii) above, there exists k0∈Nsuch that ∀t (h[k0] ⊆t →t ∈T)). Consider move(0) = μi [(τ1⊗σ)(2i+1)=0] move(n+1)=μi [i>move(n)∧(τ1⊗σ)(2i+1)=0] and take k1=move(k0−1). That is to say, player II has already played (not passed) k0times after her first k1+1 moves. Define a new strategy for player I, τ2, by putting τ2(s) =0if|s| ≤2 ·k1and τ2(s) =2 otherwise. In words, player I plays as in τ1during his first k1+1 moves and then he leaves the set A. Clearly, we have ¬A(τ2⊗I Wσ)and B(τ2⊗II Wσ). But this contradicts the fact that σis winning for player II.  Claim 5.4.2. Player II cannot have a winning strategy in GW(¬B, A). Proof. Towards a contradiction, suppose σis a winning strategy for player II in that game. As in the proof of Theorem 3.11, s ⊗II σdenotes the finite sequence consisting of player II’s moves (including 0 for representing passing) when she uses σand player I plays according to sin his first moves. Put S={s:s∈T∧∀i<|s|((s⊗II σ)(i)=2)}. In words, Scomprises those positions sin Tfor which player II either passes or chooses 0 if she uses the strategy σand player I plays according to s. Clearly, Sexists by Δ0 1-comprehension and Sis a binary tree contained in T. Let us see that Smust be infinite. Pick k1∈N. By condition i) above, there exists s1∈Tand i0∈{0, 1} such that |s1| =k2>k 1and s1∗i0 /∈T. Then, we must have ∀i <k 2(s1⊗II σ)(i) =2. For assume the contrary and suppose that there is j<k 2such that (s1⊗II σ)(j) =2. Define a strategy for player I, τ1, by putting τ1(s) =s1(k)if 2 ·k=|s| <k 2and τ1(s) =i0otherwise. (In words, player I uses s1in his first k2moves and then he leaves the set B.) It is clear that ¬B(τ1⊗I Wσ)and ¬A(τ1⊗II Wσ)hold, which is impossible since σis a winning strategy for player II. Therefore, s1is in Sand so Scontains arbitrarily long sequences, as required. Since Sis infinite, by using WKL0we get a path of S, say h ∈2N. Consider now the strategy for player I, τ2, given by τ2(s) =h(k)if |s| =2 ·k. Then we have B(τ2⊗I Wσ)and A(τ2⊗II Wσ), which again contradicts the fact that σis a winning strategy for player II.  It follows from Claims 5.4.1 and 5.4.2 that Π0 1-SLO∗ Wfails, as required.  25 Putting together Proposition 5.4 and our previous results, we obtain that Theorem 5.5. Over RCA0, the following principles are pairwise equivalent. 1. ACA0. 2. Σ0 1-Det∗ L. 3. WKL0+Σ 0 1-Det∗ W. 4. WKL0+Σ 0 1-SLO∗ L/W . Proof. Firstly, (1) ⇒(2) follows from Corollary 4.5; (2) ⇒(4) follows from Theorem 3.11 and Lemma 5.2; and (4) ⇒(1) follows from Proposition 5.4 and Lemma 5.2. Secondly, (1) ⇒(3) follows from Corollary 4.5; and (3) ⇒(1) follows from Proposition 5.4 and Lemma 5.2. It is natural to ask ourselves whether WKL0can be eliminated from items (3) and (4) of Theorem 5.5. In section 3we showed Δ0 1-Det∗ W(and, as a consequence, Δ0 1-SLO∗ W) to be rather weak (they are provable from our base theory RCA0) but the question of calibrating the exact strength of Δ0 1-SLO∗ Lover RCA0has been left pending. Note that if we were able to prove Δ0 1-SLO∗ Land WKL0to be equivalent then it would follow from Proposition 5.4 that ACA0and Σ0 1-SLO∗ Lare equivalent over the base theory RCA0. In fact, our second reversal will provide us with a characterization of ACA0in terms of SLO over plain RCA0, but it comes at a price, as we have to increase the quantifier complexity of player II’s pay-off set. Proposition 5.6. Over RCA0, (Σ0 1, Σ0 1∧Π0 1)-SLO∗ Wimplies ACA0. Proof. Assume RCA0+(Σ 0 1, Σ0 1∧Π0 1)-SLO∗ Land take ϕ(x) ∈Σ0 1(we disregard parameters). We must show that the set {x :ϕ(x)}exists. Define A(f)to be ∃k(f(k) =1 ∧∀k<k(f(k) =0))and define B(g)to be ∃k(g(k)=1∧∀k<k(g(k)=0)∧∀i≤k(g(k+i+1)=1→ϕ(i))) ∧ ∀k(g(k)=1∧∀k<k(g(k)=0)→∀i≤k(ϕ(i)→g(k+i+1)=1)). That is to say, a play for player I is in Aif it is of the form 0(k)∗1∗ffor some k∈Nand f∈2N, whereas a play for player II is in Bif it is of the form 0(l)∗1∗t0,t 1, ... ,t l∗gfor some g∈2Nand, in addition, for each i ≤l, ti=1iff ϕ(i)holds. It is clear that Ais in Σ0 1and Bis in Σ0 1∧Π0 1. Claim 5.6.1. Player II cannot have a winning strategy in the game GW(¬B, A). Proof. Towards a contradiction, suppose σis a winning strategy for player II in that game. Consider the strategy for player I given by τ1(s) =0for all s ∈Seq{0,1,2} even . Since τ1⊗I Wσ/∈B, we must have Inf(τ1, σ) and h =τ1⊗II Wσ∈A. Then, there exists k0such that h(k0) =1and ∀k<k 0(h(k) =0). Pick k1such that player II has already played (not passed) k0+1 times after her first k1moves. By bounded Σ0 1-comprehension (available in RCA0), there exists C={x :x ≤k1∧ϕ(x)}. Define a new strategy for player I, τ2, by putting τ2(s)=0 if|s|<2·k1 τ2(s)=2 if|s|=2·k1 τ2(s)=2ifi∈C 0ifi/∈Cand |s|=2·k1+2+2·iwith i≤k1 τ2(s)=0 otherwise