(CoL)

Section 3

The CoL zoo of game operations

3.1    Preview

3.2     Prefixation

3.3    Negation

3.4     Choice operations

3.5     Parallel operations

3.6     Reduction

3.7     Blind operations

3.8     Branching operations

3.9     Sequential operations

        3.10  Toggling operations

        3.11  Cirquents

3.1 Preview

As we already know, logical operators in CoL stand for operations on games. There is an open-ended pool of operations of potential interest, and which of those to study may depend on particular needs and taste. Below is an incomplete list of the operators that have been officially introduced so far.

Negation: 

Conjunctions:    (parallel),   (choice),   (sequential),   (toggling)

Disjunctions:     (parallel),   (choice),   (sequential),   (toggling)

Recurrences:   (branching),   (parallel),   (sequential),   (toggling)

Corecurrences:  (branching),   (parallel),   (sequential),   (toggling)

Universal quantifiers:    (blind),   (parallel),   (choice),   (sequential),   (toggling)

Existential quantifiers:   (blind),   (parallel),   (choice),   (sequential),   (toggling)

Implications:    (parallel),   (choice),   (sequential),  (toggling)

Rimplications:   (branching),   (parallel),   (sequential),   (toggling)

 (branching), 

 (sequential), 

 (toggling)

Among these we see all operators of classical logic, and our choice of the classical notation for them is no accident. It was pointed out earlier that classical logic is nothing but the elementary, zero-interactivity fragment of computability logic. Indeed, after analyzing the relevant definitions, each of the classically-shaped operations, when restricted to elementary games, can be easily seen to be virtually the same as the corresponding operator of classical logic. For instance, if A and B are elementary games, then so is AB, and the latter is exactly the classical conjunction of A and B understood as an (elementary) game. In a general --- not-necessarily-elementary --- case, however, ,  , ,  become more reminiscent of (yet not the same as) the corresponding multiplicative operators of linear logic. Of course, here we are comparing apples with oranges for, as noted earlier, linear logic is a syntax while computability logic is a semantics, and it may be not clear in what precise sense one can talk about similarities or differences.

In the same apples and oranges style, our operations , , ,  can be perceived  as relatives of the additive connectives and quantifiers of linear logic; , as “multiplicative quantifiers”; ,,, as “exponentials”, even though it is hard to guess which of the two groups --- , or , --- would be closer to an orthodox linear logician's heart.  On the other hand, the blind, sequential and toggling groups of operators have no counterparts in linear logic.

In this section we are going to see formal definitions of all of the above-listed operators. We agree that, throughout those definitions, Φ ranges over positions, Γ ranges over runs and e over (V,D)-valuations, where D is the domain of the game G that is being defined and V is the set of variables on which that game depends. All three metavariables should be considered universally quantified. Each definition has two clauses, one defining Lp_e^G (and thus also Lr_e^G) and the other Wn_e^G. The second clause, telling us who wins a given run Γ of G(e), always implicitly assumes that such a Γ is in Lr_e^G.

This section also provides many examples of particular games. Let us agree that, unless otherwise suggested by the context, in all those cases we have the standard universe in mind. Often we let non-numerals such as people, Turing machines, etc. act in the roles of “constants”. These should be understood as abbreviations of the corresponding decimal numerals that encode these objects in some fixed reasonable encoding. It should also be remembered that algorithmicity is a minimum requirement on ’s strategies. Some of our examples implicitly assume stronger requirements, such as efficiency or ability to act with imperfect knowledge. For instance, the problem of telling whether there is or has been life on Mars is, of course, decidable, for this is a finite problem. Yet our knowledge does not allow us to actually solve the problem. Similarly, chess is a finite game and (after ruling out the possibility of draws) one of the players does have a winning strategy in it. Yet we do not know specifically what (and which player’s) strategy is a winning one.

When omitting parentheses in compound expressions, we assume that all unary operators (negation, repudiations, recurrences, corecurrences and quantifiers) take precedence over all binary operators (conjunctions, disjunctions, implications, rimplications), among which implications and rimplications have the lowest precedence. So, for instance, A BC should be understood as A ((B)C)  rather than, say,  as (A B)C or as A ((BC)).   

Theorem 3.1.1 (proven in [Jap03, Jap08b, Jap11a]) All operators listed in this subsection preserve the static property of games (i.e., when applied to static games, the resulting game is also static). 

3.2 Prefixation

Unlike the operators listed in the preceding subsection, the operation of prefixation is not meant here to act as a logical operator in the formal language of CoL. Yet, it is very useful in characterizing and analyzing games, and we want to start our tour of the zoo with it.

Definition 3.2.1 Assume A = (Dm, Dn, Vr, A) is a game and Ψ is a unilegal position of A (otherwise the operation is undefined). The Ψ–prefixation of A, denoted 〈Ψ〉A, is defined as the game (Dm, Dn, Vr, G) such that:

• Lp_e^G={ Φ |  〈Ψ,Φ〉∈Lr_e^A};
• Wn_e^G 〈Γ〉 = Wn_e^A 〈Ψ,Γ〉.

Intuitively, 〈Ψ〉A is the game playing which means playing A starting (continuing) from position Ψ. That is, 〈Ψ〉A is the game to which A evolves (is  brought down) after the moves of Ψ have been made. Visualized as a tree, 〈Ψ〉A is nothing but the subtree of A rooted at the node corresponding to position Ψ. Below is an illustration.

3.3 Negation

For a run Γ, by Γ we mean the “negative image” of Γ (green and red interchanged). For instance,  〈α,β,γ〉 = 〈α,β,γ〉.

Definition 3.3.1  Assume A = (Dm, Dn, Vr, A) is a game.  A  (read "not A")  is defined as the game (Dm, Dn, Vr, G) such that:

• Lp_e^G={Φ | Φ∈Lp_e^A};
• Wn_e^G 〈Γ〉 =   iff   Wn_e^A 〈Γ〉 = .

In other words, A is A with the roles of the two players interchanged: Machine’s (legal) moves and wins become Environment’s moves and wins, and vice versa. So, when visualized as a tree, A is the exact negative image of A, as illustrated below:

Figure 3.3.2: Negation

Let Chess be the game of chess (with draws ruled out) from the point of view of the white player. Then  Chess is Chess “upside down”, i.e., the game of chess from the point of view of the black player:

Observe that the classical double negation principle  A = A  holds: interchanging the players’ roles twice restores the original roles of the players. It is also easy to see that we always have  〈Ψ〉A = 〈 Ψ〉 A. So, for instance, if α is Machine’s legal move in the empty position of A that brings A down to B, then the same α is Environment’s legal move in the empty position of  A, and it brings  A down to  B. Test the game A of   Figure 3.3.2 to see that this is indeed so.

3.4 Choice operations

Choice conjunction (read “chand”)  and choice disjunction (read “chor”)  combine games in the way seen below:

A  B is a game where, in the initial (empty) position, only Environment has legal moves. Such a move should be either ‘0’ or ‘1’. If Environment moves 0, the game continues as A, meaning that 〈0〉(A  B) = A; if it moves 1, then the game continues as B, meaning that 〈1〉(A  B) = B; and if it fails to make either move (“choice”), then it loses. A  B is similar, with the difference that here it is Machine who has initial moves and who loses if no such move is made.

Definition 3.4.1 Assume A₀ = (Dm, Dn, Vr₀, A₀) and A₁ =(Dm, Dn, Vr₁, A₁) are games. 

a)     A₀  A₁ is defined as the game (Dm, Dn, Vr₀∪Vr₁, G) such that:

• Lp_e^G={〈 〉} ∪ {〈i,Φ〉 |  i∈{0,1}, Φ∈Lp_e^Ai};
• Wn_e^G 〈 〉 = ;  Wn_e^G 〈i,Γ〉 = Wn_e^Ai 〈Γ〉.

b)     A₀  A₁ is defined as the game (Dm, Dn, Vr₀∪Vr₁, G) such that:

• Lp^G={〈 〉} ∪ {〈i,Φ〉 |  i∈{0,1}, Φ∈Lp^Ai};
• Wn^G 〈 〉 = ;  Wn^G 〈i,Γ〉 = Wn^Ai 〈Γ〉.

The game A of Figure 3.3.2 can now be easily seen to be (  )  ( ), and its negation be (  )  (  ). The De Morgan laws familiar from classical logic persist: we always have  (A B) = A  B and  (A  B) = A  B. Together with the earlier observed double negation principle, this means that A  B =  (A B) and A  B =  (A  B). Similarly for the quantifier counterparts   and   of  and .

Given a game A(x), the choice universal quantification (read “chall”)  xA(x) of it is nothing but the “infinite choice conjunction” A(0)A(1)A(2) …,  and the choice existential quantification (read “chexists”)   xA(x) of A(x) is the “infinite choice disjunction” A(0)A(1)A(2) …:

Specifically, xA(x) is a game where, in the initial position, only Environment has legal moves, and such a move should be one of the constants. If Environment moves c, then the game continues as A(c), and if Environment fails to make an initial move/choice, then it loses.  xA(x) is similar, with the difference that here it is Machine who has initial moves and who loses if no such move is made.  So, we always have  〈c〉xA(x)=A(c)  and 〈c〉xA(x)=A(c). Below is a formal definition of choice quantifiers.

Definition 3.4.2 Assume A(x) = (Dm, Dn, Vr, A) is a game.

a)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Lp_e^G={〈 〉} ∪ {〈c,Φ〉:   c∈Constants, Φ∈Lp_e^A(c)};
• Wn_e^G 〈 〉 = ;  Wn_e^G 〈c,Γ〉 = Wn_e^A(c)〈Γ〉.

b)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Lp_e^G={〈 〉} ∪ {〈c,Φ〉:   c∈Constants, Φ∈Lp_e^A(c)};
• Wn_e^G 〈 〉 = ;  Wn_e^G 〈c,Γ〉 = Wn_e^A(c)〈Γ〉.

Now we are already able to express traditional computational problems using formulas. Traditional problems come in two forms: the problem of computing a function f(x), or the problem of deciding a predicate p(x). The former can be written as xy(y=f(x)), and the latter as x(p(x)  p(x)). So, for instance, the constant “successor” game of Figure 2.3.4 will be written as xyA(y=x+1), and the unary “generalized successor” game of Figure 2.3.5 as xyA(y=x+z).  The following game, which is about deciding the “evenness” predicate, could be written as  x(y(x=2y)  y(x=2y)) ( will be officially defined later, but, as promised, its meaning is going to be exactly classical when applied to an elementary game like  x=2y). 

Classical logic has been repeatedly criticized for its operators not being constructive. Consider, for example, xy(y=f(x)). It is true in the classical sense as long as f is a total function. Yet its truth has little (if any) practical import, as “y” merely signifies existence of y, without implying that such a y can actually be found. And, indeed, if f is an incomputable function, there is no method for finding y. On the other hand, the choice operations of CoL are constructive. Computability (“truth”) of  xy(y=f(x)) means more than just existence of y; it means the possibility to actually find (compute, construct) a corresponding y for every x.

 xy(Halts(x,y)  Halts(x,y))    xy(Halts(x,y)  Halts(x,y)).

Chess   Chess, on the other hand, is an example of a computable-in-principle yet “practically incomputable” problem, with no real computer anywhere close to being able to handle it.

There is no need to give a direct definition for the remaining choice operation of choice implication (“chimplication”), for it can be defined in terms of ,  in the “standard” way:

Definition 3.4.3 AB  =_def   A B.

Each of the other sorts of disjunctions (parallel, sequential and toggling) generates the corresponding implication the same way.

3.5 Parallel operations

The parallel conjunction (read “pand”) AB and the parallel disjunction (read “por”)  AB of A and B are games playing which means playing the two games simultaneously. In order to win in AB [resp. AB],  needs to win in both [resp. at least one] of the components A,B. For instance, ChessChess is a two-board game, where  plays black on the left board and white on the right board, and where it needs to win in at least one of the two parallel sessions of chess. A win can be easily achieved here by just mimicking in Chess the moves that the adversary makes in Chess, and vice versa. This copycat strategy guarantees that the positions on the two boards always remain symmetric, as illustrated below, and thus  eventually loses on one board but wins on the other. 

This is very different from Chess  Chess. In the latter  needs to choose between the two components and then win the chosen one-board game, which makes Chess  Chess essentially as hard to win as either Chess or Chess. A game of the form AB is generally easier (at least, not harder) to win than AB, the latter is easier to win than AB, and the latter in turn is easier to win than AB.

Technically, a move α in the left [resp. right] -conjunct or -disjunct is made by prefixing α with ‘0.’ [resp. ‘1.’]. For instance, in (the initial position of) (AB)(CD), the move ‘1.0’ is legal for , meaning choosing the left -conjunct in the second -disjunct of the game. If such a move is made, the game continues as (AB)C. The player , too, has initial legal moves in (AB)(CD), which are ‘0.0’ and ‘0.1’.

In the formal definitions of this section and throughout the rest of this webpage, we use the important notational convention according to which:

Notation 3.5.1 For a run Γ and string α,  Γ ^α means  the result of removing from Γ all moves except those of the form αβ,  and then deleting the prefix ‘α’ in the remaining moves.

So, for instance, 〈1.2,1.0,0.33〉^1.  = 〈2,0〉  and  〈1.2,1.0,0.33〉^0. = 〈33〉. Another example:  where Γ is the leftmost branch of the tree for (  ) (  ) shown in Figure 3.5.3, we have Γ^0. =  〈0〉 and Γ^1. = 〈0〉. Intuitively, we see this Γ as consisting of two subruns, one (Γ^0.) being a run in the first -disjunct of (  ) (  ) , and the other (Γ^1.) being a run in the second disjunct.

Definition 3.5.2 Assume A₀ = (Dm, Dn, Vr_0,  A₀) and A₁ = (Dm, Dn, Vr_1,  A₁) are games.

a)     A₀A₁ is defined as the game (Dm, Dn, Vr₀∪Vr₁, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘0.’ or ‘1.’ and,  for both i∈{0,1},  Φ^i.∈ Lp_e^Ai;
• Wn_e^G 〈Γ〉 =  iff, for both i∈{0,1},  Wn_e^Ai 〈Γ^i.〉=.

b)     A₀A₁ is defined as the game (Dm, Dn, Vr₀∪Vr₁, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘0.’ or ‘1.’ and,  for both i∈{0,1},  Φ^i. ∈ Lp_e^Ai;
• Wn_e^G 〈Γ〉= iff, for both i∈{0,1},  Wn_e^Ai 〈Γ^i.〉=.

When A and B are (constant) finite games, the depth of AB or AB is the sum of the depths of A and B, as seen below.

 Figure 3.5.3: Parallel disjunction

This signifies an exponential growth of the breadth, meaning that, once we have reached the level of parallel operations, continuing drawing trees in the earlier style becomes no fun. Not to be disappointed though: making it possible to express large- or infinite-size game trees in a compact way is what our game operators are all about after all.

Whether trees are or are not helpful in visualizing parallel combinations of unistructural games, prefixation is still very much so if we think of each unilegal position Φ of A as the game  〈Φ〉A. This way, every unilegal run G of A becomes a sequence of games as illustrated in the following example.

Example 3.5.4   To the (uni)legal run Γ = 〈1.7, 0.7, 0.49, 1.49〉  of game A = xy(y≠x²)  xy(y=x²) induces the following sequence, showing how things evolve as Γ runs, i.e., how the moves of Γ affect/modify the game that is being  played:

• xy(y≠x²)  xy(y=x²)    i.e. A
• xy(y≠x²)  y(y=7²)        i.e. 〈1.7〉A
• y(y≠7²)  y(y=7²)            i.e. 〈1.7,0.7〉A
• 49≠7²  y(y=7²)                 i.e. 〈1.7,0.7,0.49〉A
• 49≠7²  49=7²                      i.e. 〈1.7,0.7,0.49,1.49〉A

The run hits the true proposition 49≠7²  49=7², and hence is won by the machine.

As we may guess, the parallel universal quantification (“pall”) xA(x) of A(x) is nothing but A(0)A(1)A(2) … and the parallel existential quantification (“pexists”) xA(x) of A(x) is nothing but A(0)A(1)A(2)…

Definition 3.5.5 Assume A(x) = (Dm, Dn, Vr, A) is a game.

a)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘c.’ for some c∈Constants and, for all such c, Φ^c. ∈ Lp_e^A(c);
• Wn_e^G 〈Γ〉 =  iff, for all c∈Constants, Wn_e^A〈Γ^c.〉=.

b)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘c.’ for some c∈Constants and, for all such c, Φ^c. ∈ Lp_e^A(c);
• Wn_e^G 〈Γ〉= iff, for all c∈Constants, Wn_e^A〈Γ^c.〉=.
  

The next group of parallel operators are parallel recurrence (“precurrence”)  and parallel corecurrence (“coprecurrence”) .  A is nothing but the infinite parallel conjunction AAA…, and A is the infinite parallel disjunction AAA…. Equivalently, A and A can be respectively understood as xA and xA, where x is a dummy variable on which A does not depend. Intuitively, playing A means simultaneously playing in infinitely many “copies” of A, and  is the winner iff it wins A in all copies. A is similar, with the only difference that here winning in just one copy is sufficient.

Definition 3.5.6 Assume A = (Dm, Dn, Vr, A) is a game.

a)     A is defined as the game (Dm, Dn, Vr, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘c.’ for some c∈Constants and, for all such c, Φ^c. ∈ Lp_e^A;
• Wn_e^G 〈Γ〉 =  iff, for all c∈Constants, Wn_e^A〈Γ^c.〉=.

b)     A is defined as the game (Dm, Dn, Vr, G) such that:

• Φ∈Lp_e^G iff every move of Φ has the prefix ‘c.’ for some c∈Constants and, for all such c, Φ^c. ∈ Lp_e^A;
• Wn_e^G 〈Γ〉 =  iff, for all c∈Constants, Wn_e^A〈Γ^c.〉=.

As was the case with choice operations, we can see that the definition of each parallel operation seen so far in this section can be obtained from the definition of its dual by just interchanging  with . Hence it is easy to verify that we always have  (A B) = AB,  (A B) = AB,  xA(x) = xA(x),  xA(x) = xA(x),  A = A,  A = A, This, in turn, means that each parallel operation is definable in the standard way in terms of its dual operation and negation. For instance, AB can be defined as (AB), and A as A. Three more parallel operations defined in terms of negation and other parallel operations are   parallel implication (“pimplication”) ,  parallel rimplication (“primplication”)   and  parallel repudiation (“prepudiation”) . Here the prefix “p”, as before, stands for “parallel”, and the prefix “r” in “rimplication” stands for “recurrence”. 

Definition 3.5.7    a) A  B  =_def   A  B

                              b) A  B  =_def  A  B

                              c)  A  =_def  A

Note that, just like negation and unlike choice operations, parallel operations preserve the elementary property of games. When restricted to elementary games, the meanings of ,  and  coincide with those of classical conjunction, disjunction and implication. Further, as long as all individuals of the universe have naming constants,  the meanings of  and  coincide with those of classical universal quantifier and existential quantifier. The same conservation of classical meaning (but without any conditions on the universe) is going to be the case with the blind quantifiers , defined later; so, at the elementary level, when all individuals of the universe have naming constants,  and  are indistinguishable from  and , respectively. As for the parallel recurrence and corecurrence, for an elementary A we simply have A=A=A. 

While all classical tautologies automatically remain valid when parallel operators are applied to elementary games, in the general case the class of valid (“always computable”) principles shrinks. For example, P PP, i.e. P(PP), is not valid.  Back to our chess example, one can see that the earlier copycat strategy successful for ChessChess would be inapplicable to Chess(ChessChess). The best that  can do in this three-board game is to  synchronize Chess with one of the two conjuncts of ChessChess. It is possible that then Chess and the unmatched Chess are both lost, in which case the whole game will be lost.

The principle P PP is valid in classical logic because the latter sees no difference between P and PP. On the other hand, in virtue of its semantics, CoL is resource-conscious, and in it P is by no means the same as PP or PP.  Unlike P PP,  P PP is a valid principle. Here, in the antecedent, we have infinitely many “copies” of P. Pick any two copies and, via copycat, synchronize them with the two conjuncts of the consequent. A win is guaranteed.

3.6 Reduction

Intuitively, AB is the problem of reducing B to A: solving AB means solving B while having A as a computational resource. Specifically,  may observe how A is being solved (by the environment), and utilize this information in its own solving B. As already pointed out, resources are symmetric to problems: what is a problem to solve for one player is a resource that the other player can use, and vice versa. Since A is negated in AB and negation means switching the roles, A appears as a resource rather than problem for  in AB.  Our copycat strategy for ChessChess was an example of reducing Chess to Chess. The same strategy was underlying Example 3.5.4, where xy(y=x²) was reduced to itself.

Let us look at a more meaningful example: reducing the acceptance problem to the halting problem. The former, as a decision problem, will be written as xy (Accepts(x,y)  Accepts(x,y)), where Accepts(x,y) is the predicate “Turing machine x accepts input y”. Similarly, the halting problem is written as xy (Halts(x,y)  Halts(x,y)). Neither problem has an algorithmic solution, yet the following pimplication does:

xy (Halts(x,y)  Halts(x,y))  xy (Accepts(x,y)  Accepts(x,y))

Here is Machine’s winning strategy for the above game. Wait till Environment makes moves 1.m and 1.n for some m and n. Making these moves essentially means asking the question “Does machine m accept input n?”.  If such moves are never made, you win. Otherwise, the moves bring the game down to

xy (Halts(x,y)  Halts(x,y))  Accepts(m,n)  Accepts(m,n)

Make the moves 0.m and 0.n, thus asking the counterquestion “Does machine m halt on input n?”.  Your moves bring the game down to 

Halts(m,n)  Halts(m,n) Accepts(m,n)  Accepts(m,n)

Environment will have to answer this question, or else it loses (why?). If it answers by move 0.0 (“No, m does not halt on n”), you make the move 1.0 (say “m does not accept n”). The game will be brought down to Halts(m,n) Accepts(m,n). You win, because if m does not halt on n, then it does not accept n, either. Otherwise, if Environment answers by move 0.1 (“Yes, m halts on n”), start simulating m on n until m halts. If you see that m accepted n, make the move 1.1 (say “m accepts n”); otherwise make the move 1.0 (say “m does not accept n”). Of course, it is a possibility that the simulation goes on forever. But then Environment has lied when saying “m halts on n”; in other words, the antecedent is false, and you still win.  

Note that what Machine did when following the above strategy was indeed reducing the acceptance problem to the halting problem: it solved the former using an external (Environment-provided) solution of the latter.

There are many natural concepts of reduction, and a strong case can be made in favor of the thesis that  the sort of reduction captured by  is most basic among them. For this reason, we agree that, if we simply say “reduction”, it always means the sort of reduction captured by  . A great variety of other reasonable concepts of reduction is expressible in terms of .  Among those is Turing reduction. Remember that a predicate q(x) is said to be Turing reducible to a predicate p(x) if q(x) can be decided by a Turing machine equipped with an oracle for p(x).  For a positive integer n, n-bounded Turing reducibility is defined in the same way, with the only difference that here the oracle is allowed to be used only n times. It turns out that parallel rimplication  is a conservative generalization of Turing reduction. Namely, when p(x) and q(x) are elementary games (i.e. predicates), q(x) is Turing reducible to p(x) if and only if the problem x(p(x) p(x))  x(q(x)  q(x)) has an algorithmic solution. If here we change  back to , we get the same result for 1-bounded Turing reducibility. More generally, as one might guess, n-bounded Turing reduction will be captured by

x₁(p(x₁)  p(x₁))  …  x_n(p(x_n)  p(x_n)) x(q(x) q(x)).

If, instead, we write 

x₁…x_n((p(x₁)  p(x₁)) …  (p(x_n) p(x_n))) x(q(x) q(x)),

then we get a conservative generalization of n-bounded weak truth-table reduction. The latter differs from n-bounded Turing reduction in that here all n oracle queries should be made at once, before seeing responses to any of those queries. What is called mapping (many-one) reducibility of q(x) to p(x) is nothing but computability of xy(q(x)↔p(y)), where A↔B abbreviates (AB)(BA).  We could go on and on with this list.

And yet many other natural concepts of reduction expressible in the language of CoL  may have no established names in the literature. For example, from the previous discussion it can be seen that a certain reducibility-style relation holds between the predicates Accepts(x,y) and Halts(x,y) in an even stronger sense than the algorithmic winnability of

xy (Halts(x,y)  Halts(x,y)) xy (Accepts(x,y)  Accepts(x,y)).

In fact, not only the above problem has an algorithmic solution, but also the generally harder-to-solve problem

 xy (Halts(x,y) Halts(x,y) Accepts(x,y)  Accepts(x,y)).

Among the merits of CoL is that it offers a formalism and deductive machinery for systematically expressing and studying computation-theoretic relations such as reducibility, decidability, enumerability, etc., and all kinds of variations of such concepts.

Back to reducibility, while the standard approaches only allow us to talk about (a whatever sort of) reducibility as a relation between problems, in our approach reduction becomes an operation on problems, with reducibility as a relation simply meaning computability of the corresponding combination (such as AB) of games. Similarly for other relations or properties such as the property of decidability. The latter becomes the operation of deciding if we define the problem of deciding a predicate (or any computational problem) p(x) as the game x(p(x) p(x)). So, now we can meaningfully ask questions such as “Is the reduction of the problem of deciding q(x) to the problem of deciding p(x) always reducible to the mapping reduction of q(x) to p(x)?”. This question would be equivalent to whether the following formula is valid in CoL:

xy(q(x) ↔ p(y)) (x(p(x)  p(x)) x(q(x)  q(x))).

The answer turns out to be “Yes”, meaning that mapping reduction is at least as strong as reduction. Here is a strategy which wins this game no matter what particular predicates p(x) and q(x) are: 

1. Wait till, for some m, Environment brings the game down to  

xy(q(x) ↔ p(y)) (x(p(x)  p(x)) q(m)  q(m)).

2. Bring the game down to  

y(q(m) ↔ p(y)) (x(p(x)  p(x)) q(m)  q(m)).

3. Wait till, for some n, Environment brings the game down to  

 (q(m) ↔ p(n)) (x(p(x)  p(x)) q(m)  q(m)).

4. Bring the game down to  

(q(m) ↔ p(n)) (p(n)  p(n) q(m)  q(m)).

5. Wait till Environment brings the game down to one of the following:  

      5a. (q(m) ↔ p(n)) (p(n) q(m)  q(m)). In this case, further bring it down to (q(m) ↔ p(n)) (p(n) q(m)), and you have won.

      5b. (q(m) ↔ p(n)) (p(n) q(m)  q(m)). In this case, further bring it down to (q(m) ↔ p(n)) (p(n) q(m)), and you have won, again.

We can also ask: “Is the mapping reduction of q(x) to p(x) always reducible to the reduction of the problem of deciding q(x) to the problem of deciding p(x)?”. This question would be equivalent to whether the following formula is valid:

( x(p(x)  p(x)) x(q(x)  q(x)))   xy(q(x) ↔ p(y)).

The answer here turns out to be “No”, meaning that mapping reduction is properly stronger than reduction. This negative answer can be easily obtained by showing that the above formula is not provable in the deductive system CL4 that we are going to see later. CL4 is sound and complete with respect to validity. Its completeness implies that any formula which is not provable in it (such as the above formula) is not valid. And the soundness of CL4 implies that every provable formula is valid. So, had our ad hoc attempt to come up with a strategy for xy(q(x) ↔ p(y)) (x(p(x)  p(x)) x(q(x)  q(x))) failed, its validity could have been easily established by finding a CL4-proof of it.

To summarize, CoL offers not only a convenient language for specifying computational problems and relations or operations on them, but also a systematic tool for answering questions in the above style and beyond.

3.7 Blind operations

Our definition of the blind universal quantifier (“blall”) x and blind existential quantifier (“blexists”) x assumes that the game A(x) to which they are applied satisfies the condition of unistructurality in x. This condition is weaker than the earlier seen unistructurality: every unistructural game is also unistructural in x, but not vice versa. Intuitively, unistructurality in x means that the structure of the game does not depend on (how the valuation evaluates) the variable x. Formally, we say that a game A(x)=(Dm,Dn,Vr,A)  is unistructural in x iff, for any (Vr,Dm)-valuation e and any two individuals a and b, we have Lr_e^A(a) = Lr_e^A(b).  All constant or elementary games are unistructural in (whatever variable) x. And all operations of CoL are known to preserve unistructurality in x. 

Definition 3.7.1 Assume A(x) = (Dm, Dn, Vr, A) is a game unistructural in x.

a)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Lp_e^G= Lp_e^A(x);
• Wn_e^G 〈Γ 〉 =  iff, for all a∈Dm,  Wn_e^A(a) 〈Γ〉 = .

b)     xA(x)  is defined as the game (Dm, Dn, Vr-{x}, G) such that:

• Lp_e^G= Lp_e^A(x);
• Wn_e^G 〈Γ〉 =   iff, for all a∈Dm,  Wn_e^A(a) 〈Γ〉 =.

Intuitively, playing xA(x) or xA(x) means just playing A(x) “blindly”, without knowing the value of x. In xA(x), Machine wins iff the play it generates is successful for every possible value of x from the domain, while in xA(x) being successful for just one value is sufficient. When applied to elementary games, the blind quantifiers act exactly like the quantifiers of classical logic, even if not all individuals of the universe have naming constants.