Giorgi Japaridze's  page for

Computability Logic

გამოთვლადობის ლოგიკა

Логика вычислимости



NOTE: This site should be viewed with Internet Explorer. Other browsers may fail to display formulas properly. 

Computability is one of the most interesting and fundamental concepts in mathematics and computer science, and it is natural to ask what logic it induces. This is where Computability Logic (CoL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, CoL is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme “from truth to computability”.

Under the approach of CoL, logical operators stand for operations on computational problems, formulas represent such problems, and their “truth” is seen as algorithmic solvability. In turn, computational problems --- understood in their most general, interactive sense --- are defined as games played by a machine against its environment, with “algorithmic solvability” meaning existence of a machine that wins the game against any possible behavior of the environment. With this semantics, CoL provides a systematic answer to the question “what can be computed?”, just like classical logic is a systematic tool for telling what is true. Furthermore, as it happens, in positive cases “what can be computed” always allows itself to be replaced by “how can be computed”, which makes CoL of potential interest in not only theoretical computer science, but many applied areas as well, including constructive applied theories, interactive knowledge base systems, resource oriented systems for planning and action, or declarative programming languages.

Currently CoL is still at an early stage of development, with open problems prevailing over answered questions. For this reason it offers plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science. Come and join!



1    The philosophy of CoL

1.1     Syntax vs. semantics

1.2     Why game semantics?

1.3     CoL vs. classical logic

1.4     CoL vs. linear logic

1.5     CoL vs. intuitionistic logic

1.6     CoL vs. independence-friendly logic

1.7   The ‘from semantics to syntax’ paradigm

2    Games

2.1     The two players

2.2     Moves, runs and positions

2.3     Constant games

2.4     Not-necessarily-constant games

2.5     Static games

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 quantifiers

3.8     Branching operations

3.9     Sequential operations

        3.10  Toggling operations

        3.11  Cirquents

4    Interactive machines

  4.1   Interactive computability

  4.2   Interactive complexity

5    The language of CoL and its semantics

        5.1   Formulas

        5.2   Interpretations

        5.3   Validity

6    Axiomatizations

        6.1   Outline

        6.2   The Gentzen-style system CL7

        6.3   The Gentzen-style system Int+ 

        6.4   The cirquent calculus system CL15 

        6.5   The brute force system CL13

        6.6   The brute force system CL4

        6.7   The brute force system CL12

7    Clarithmetic (CoL-based arithmetic)

       7.1   Introduction

        7.2   Clarithmetic versus bounded arithmetic

        7.3   Motivations

        7.4   Common preliminaries for all our theories of clarithmetic

        7.5   Clarithmetics for polynomial time, polynomial space, elementary and primitive recursive computability

        7.6   Clarithmetics for provable computability

        7.7   Tunable clarithmetic

8    CoL-based knowledgebase and resourcebase systems

9    Literature

      9.1   Selected papers on CoL by Japaridze

      9.2   Selected papers on CoL by other authors

      9.3   PhD theses, MS theses and externally funded projects on CoL

      9.4   Lecture notes on CoL, presentations and other links

      9.5   Additional references





1 The philosophy of CoL

1.1 Syntax vs. semantics

A starting philosophical point of CoL is that syntax --- the study of axiomatizations or other string-manipulation systems --- exclusively owes its right on existence to semantics,  and is thus secondary to it. Logic is meant to be the most basic, general-purpose formal tool potentially usable by intelligent agents in successfully navigating the real life. And it is semantic that establishes that ultimate real-life meaning of logic. Syntax is important, yet it is so not in its own right but only as much as it serves a meaningful semantics, allowing us to realize the potential of that semantics in some systematic and perhaps convenient or efficient way. Not passing the test for soundness with respect to the underlying semantics would fully disqualify any syntax, no matter how otherwise appealing it is. Note --- disqualify the syntax and not the semantics. Why this is so hardly requires any explanation. Relying on an unsound syntax might result in wrong beliefs, misdiagnosed patients or crashed spaceships. An incomplete syntax, on the other hand, potentially means missing benefits that should not have been missed.

A separate question, of course, is what counts as a semantics. The model example of a semantics with a capital ‘S’ is that of classical logic. But in the logical literature this term often has a more generous meaning than what CoL is ready to settle for. As pointed out, CoL views logic as a universal-utility tool. So, a capital-‘S’-semantics should be non-specific enough, and applicable to the world in general rather than some very special and artificially selected (worse yet, artificially created) fragment of it. Often what is called a semantics is just a special-purpose apparatus designed to help analyze a given syntactic construction rather than understand and navigate the outside world. The usage of Kripke models as a derivability test for intuitionistic formulas, or as a validity criterion in various systems of modal logic is an example. An attempt to see more than a technical, syntax-serving instrument in this type of lowercase-‘s’-semantics might create a vicious circle: a deductive system L under question is “right” because it derives exactly the formulas that are valid in a such and such Kripke semantics; and then it turns out that the reason why we are considering the such and such Kripke semantics is that ... it validates exactly what L derives. 


1.2 Why game semantics?

For CoL, a game are not just a game.  It is a foundational mathematical concept on which a powerful enough logic (=semantics) should be based. This is so because, as noted, CoL sees logic as a “real-life navigational tool”, and it is games that appear to offer the most comprehensive, coherent, natural, adequate and convenient mathematical models for the very essence of all “navigational” activities of agents: their interactions with the surrounding world. An agent and its environment  translate into game-theoretic terms as two players; their actions as moves; situations arising in the course of interaction as  positions; and success or failure as wins or losses.

It is natural to require that the interaction strategies of the party that we have referred to as an “agent” be limited to algorithmic ones, allowing us to henceforth call that player a machine.  This is a minimum condition that any non-esoteric game semantics would have to satisfy. On the other hand, no restrictions can or should be imposed on the environment, who represents a capricious user, the blind forces of nature, or the devil himself. Algorithmic activities being synonymous to computations, games thus represent computational problems --- interactive tasks performed by computing agents, with computability meaning winnability, i.e. existence of a machine that wins the game against any possible (behavior of the) environment.

In the 1930s, in the form of the famous Church-Turing thesis, mankind came up with what has been perceived as an ultimate mathematical definition of the precise meaning of algorithmic solvability. Curiously or not, such a definition was set forth and embraced before really having attempted to answer the seemingly more basic question about what computational problems are --- the very entities that may or may not have algorithmic solutions in the first place. The tradition established since then in theoretical computer science by computability simply means Church-Turing computability of functions, as the task performed by every Turing machine is nothing but receiving an input x and generating the output f(x) for some function f.

Yet most tasks that computers and computer networks perform are interactive, with strategies not always allowing themselves to be adequately understood as functions. To understand this, it would be sufficient to just reflect on the behavior of one's personal computer. The job of your computer is to play one long game against you. Now, have you noticed your faithful servant getting slower every time you use it? Probably not. That is because the computer is smart enough to follow a non-functional strategy in this game. If its strategy was a function from positions (interaction histories) to moves, the response time would inevitably keep worsening due to the need to read the entire, continuously lengthening interaction history every time before responding. Defining strategies as functions of only the latest moves is also not a way out. The actions of your computer certainly depend on more than your last keystroke.

Two main concepts on which the semantics of CoL is based are those of static games (defined later) and their winnability. Correspondingly, the philosophy of CoL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:

Thesis 1.2.1

      (1) The concept of static games is an adequate formal counterpart of our intuition of (“pure”, speed-independent) interactive computational problems.

   (2) The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.


So far games in logic have been mostly used to find models and semantical justifications for syntactically introduced popular systems such as intuitionistic logic or linear logic. For instance: Lorenzen’s [Lor61, Fel85] game semantics was created for the purpose of justifying intuitionistic logic; Hintikka’s [Hin73] game-theoretic semantics was originally meant to provide an alternative semantics for classical logic; Blass’ [Bla92] game semantics was mainly motivated by the needs of linear logic, and so were the game-semantical approaches elaborated by Abramsky, Jagadeessan [Abr94] and others. In this respect, CoL turns the tables around and views games as foundational entities in their own right.  It starts with identifying the most basic and meaningful operations on games. Understand those operations as logical operators, it then look at the logics induced by the corresponding concept of validity, regardless of how unusual such logics may turn out. There is no target syntactic construction to serve.


1.3 CoL vs. classical logic

Computability in the traditional Church-Turing sense is a special case of winnability --- winnability restricted to two-step (input/output, question/answer) interactive problems. So is the classical concept of truth, which is nothing but winnability restricted to propositions, viewed by CoL as zero-step problems, i.e., games with no moves that are automatically won by the machine when true and lost when false. This way, the game  semantics of CoL is a generalization, refinement and conservative extension of that of classical logic.

Thinking of a human user in the role of the environment, computational problems are synonymous to computational tasks --- tasks performed by a machine for the user/environment. What is a task for a machine is then a resource for the environment, and vice versa. So the CoL games, at the same time, formalize our intuition of computational resources. Logical operators are understood as operations on such  tasks/ resources/games, atoms as variables ranging over tasks/resources/games, and validity of a logical formula as being “always winnable”, i.e. as existence --- under every particular interpretation of atoms --- of a machine that successfully accomplishes/provides/wins the corresponding task/resource/game no matter how the environment behaves.  It is this approach that makes CoL “a formal theory of computability in the same sense as classical logic is a formal theory of truth”. Furthermore, as mentioned, the classical concept of truth is a special case of winnability, which eventually translates into classical logic’s being nothing but a special fragment of computability logic. 


1.4 CoL vs. linear logic

CoL is a semantically conceived logic, and so far its syntax has only been partially  developed.  In a sense, this situation is opposite to the case with linear logic [Gir87], where a “full” syntactic construction existed right at the beginning, but where a really good formal semantics convincingly justifying the resource intuitions traditionally associated with that construction is still being looked for. In fact, the semantics of CoL can be seen to be providing such a justification, although only in a limited sense explained below.

The set of valid formulas in a certain fragment of the otherwise more expressive language of CoL forms a logic which is similar to but by no means the same as linear logic.  When no exponentials are involved, the two logics typically agree on short and simple formulas. For instance, both logics reject  P  P  P   and accept P  P  P, with classical-shape propositional connectives here and later understood as the corresponding multiplicative operators of linear logic, and square-shape operators as additives ( = “with”,  = “plus”). Similarly, both logics reject P  P and accept P  P. On the other hand, CoL disagrees with linear logic on many more evolved formulas. E.g., CoL validates the following two principles rejected even by affine logic, i.e., linear logic with the weakening rule:

(P  Q)  (R  S)     (P  R)  (Q  S)  (Blass’s [Bla92] principle);

(P  (R  S))  (Q  (R  S))  ((P  Q)  R)  ((P  Q)  S)    (P  Q)  (R  S).

With  and , which are CoL’s counterparts of the exponentials !,? of linear logic,  disagreements can be observed already at the level of very short formulas, such as P  P. Generally, every formula provable in affine logic is valid in CoL but not vice versa.  

Neither the similarities nor the discrepancies are a surprise. The philosophies of CoL and linear logic overlap in their pursuit to develop a logic of resources. But the ways this philosophy is materialized are rather different. CoL starts with a mathematically strict and intuitively convincing semantics, and only after that, as a natural second step, asks what the corresponding logic and its possible axiomatizations are. On the other hand, it would be accurate to say that linear logic started directly from the second step. Even though certain companion semantics were provided for it from the very beginning, those are not quite what we earlier agreed to call capital-‘S’. As a formal theory of resources (rather than that of phases or coherence spaces), linear logic has been motivated and introduced syntactically rather than semantically, essentially by taking classical sequent calculus and deleting the rules that seemed unacceptable from a certain intuitive, naive resource point of view. Hence, in the absence of a clear formal concept of resource-semantical truth or validity, the question about whether the resulting system was complete could not even be meaningfully asked. In this process of syntactically rewriting classical logic some innocent, deeply hidden principles could have easily gotten victimized. CoL believes that this is exactly what happened, with the above-mentioned formulas separating it from linear logic, along with many other principles, viewed as babies thrown out with the bath water. Of course, many retroactive attempts have been made to find semantical (often game-semantical) justifications for linear logic. Technically it is always possible to come up with some sort of a formal semantics that matches a given target syntactic construction, but the whole question is how natural and meaningful such a semantics is in its own rights, and how adequately it corresponds to the logic’s underlying philosophy and ambitions. Unless, by good luck, the target system really is “the right logic”, the chances of a decisive success when following the odd scheme from syntax to semantics could be rather slim. The natural scheme is from semantics to syntax. It matches the way classical logic evolved and climaxed in Gödel’s completeness theorem. And, as we now know, this is exactly the scheme that computability logic, too, follows.

With the two logics in a sense competing for the same market, the main --- or perhaps only --- advantage of linear logic over CoL is its having a nice and simple syntax. In a sense, linear logic is (rather than has) a beautiful syntax; and computability logic is (rather than has) a meaningful semantics. An axiomatization of CoL in the full generality of its language has not been found yet. Only certain fragments of it have been axiomatized, including the one corresponding to the multiplicative-additive fragment of linear logic. Such axiomatizations tend to be more involved than that of linear logic, so the syntactic simplicity advantage of linear logic will always remain. Well, CoL has one thing to say: simplicity is good, yet, if it is most important, then nothing can ever beat ... the empty logic.

From CoL’s perspective, classical logic and (loosely understood) linear logic can be seen as two extremes within its all-unifying resource- (game-) semantical vision. Specifically, the main difference between linear logic and classical logic is that the former sees all occurrences of the same atom in a formula as different copies of the same resource, while the latter sees such occurrences as the same single copy, simply written at different places for technical reasons.  So, linear logic rejects $1$1$1 because in the antecedent we have one dollar while in the consequent two, with the possibility to buy an apple with one and an orange with the other. On the other hand, classical logic accepts thus principle because it sees a single dollar in the consequent, written twice for some strange reason; if the first conjunct of the consequent is spent buying an apple, the second conjunct is also automatically spent on the same apple, with no money remaining for oranges. As for CoL, it allows us to write expressions where all occurrences of $1 stand for the same one-dollar bill, or all stand for separate bills, or we have a mixture of these two, where some occurrences stand for the same bill while some other occurrences in the same expression stand for different bills.

Blass [Bla92] was the first to attempt a game-semantical justification for linear logic. This goal was only partially achieved, as the resulting logic, just like the above-discussed fragment of CoL, turned out to validate more principles than linear logic does. It should be pointed out that the multiplicative-additive fragment of the logic induced by Blass’ semantics coincides with the corresponding fragment of CoL. This does not extend to the full language of linear logic though. For instance, Blass’ semantics validates the following principle which is invalid in CoL: [Jap12a] 

P  ((P  P  P)  (P  P  P))    P.

In full generality, the “linear-logic fragment” of CoL is strictly between linear logic and the logic induced by Blass’ semantics.[Jap09a]


1.5 CoL vs. intuitionistic logic

From CoL’s perspective, the situation with intuitionistic logic [Hey71] is rather similar to what we had with linear logic. Intuitionistic logic is another example of a syntactically conceived logic. Despite decades of efforts, no fully convincing semantics has been found for it. Lorenzen’s [Lor61] game semantics, which has a concept of validity without having a concept of truth, has been perceived as a technical supplement to the existing syntax rather than as having independent importance. Some other semantics, such as Kleene’s realizability [Kle52] or Gödel’s Dialectica interpretation [Göd58], are closer to what we might qualify as capital-‘S’. But, unfortunately, they validate certain principles unnegotiably rejected by intuitionistic logic.

Just like this was the case with linear logic, the set of valid formulas in a certain fragment of the language of CoL forms a logic which is properly stronger[Mez10, Jap07b] than Heyting’s intuitionistic logic. However, the two come “much closer” to each other than CoL and linear logic do. The shortest known formula separating intuitionistic logic from the corresponding fragment of CoL is

((P  )  Q  R)  (((P  )  )  S  T)  ((P  )  Q)  ((P  )  R)  (((P  )  )  S)  (((P  )  )  T),

where , , ,  are CoL’s counterparts of the intuitionistic implication, absurd, disjunction and conjunction, respectively.

Just like the resource philosophy of CoL overlaps with that of linear logic, so does its algorithmic philosophy with the constructivistic philosophy of intuitionism. The difference, again, is in the ways this philosophy is materialized.  Intuitionistic logic has come up with a “constructive syntax” without having an adequate underlying formal semantics, such as a clear concept of truth in some constructive sense. This sort of a syntax was essentially obtained from the classical one by banning the offending law of  the excluded middle. But, as in the case of linear logic, the critical question immediately springs out: where is a guarantee that together with excluded middle some innocent principles would not be expelled as well? The constructivistic claims of CoL, on the other hand, are based on the fact that it defines truth as algorithmic solvability. The philosophy of CoL does not find the term constructive syntax meaningful unless it is understood as soundness with respect to some constructive semantics, for only a semantics may or may not be constructive in a reasonable sense. The reason for the failure of P  P in CoL is not that this principle ... is not included in its axioms. Rather, the failure of this principle is exactly the reason why this principle, or anything else entailing it, would not be among the axioms of a sound system for CoL. Here “failure” has a precise semantical meaning. It is non-validity, i.e. existence of a problem A for which A  A is not algorithmically solvable. 

It is also worth noting that, while intuitionistic logic irreconcilably defies classical logic, computability logic comes up with a peaceful solution acceptable for everyone. The key is the expressiveness of its language, that has (at least) two versions for each traditionally controversial logical operator, and particularly the two versions  and  of disjunction. The semantical meaning of  conservatively extends --- from moveless games to all games --- its classical meaning, and the principle P  P survives as it represents  an always-algorithmically-solvable combination of problems, even if solvable in a sense that some constructivistically-minded might pretend to fail to understand. And the semantics of , on the other hand, formalizes and conservatively extends a different, stronger meaning which apparently every constructivist associates with disjunction. As expected, then P  P turns out to be semantically invalid. CoL's proposal for settlement between classical and constructivistic logics then reads: ‘If you are open (=classically) minded, take advantage of the full expressive power of CoL; and if you are constructivistically minded, just identify a collection of the operators whose meanings seem constructive enough to you, mechanically disregard everything containing the other operators, and put an end to those fruitless fights about what deductive methods or principles should be considered right and what should be deemed wrong’.


1.6 CoL vs. independence-friendly logic

Relatively late developments [Jap06c, Jap11b, Xu14] in CoL made it possible to switch from formulas to the more flexible and general means of expression termed cirquents. The main distinguishing feature of the latter is that they allow to account for various sorts of sharing between subexpressions. After such a generalization, independence-friendly (IF) logic [Hin73] became a yet another natural fragment of CoL.[Jap11b, Xu14, Xu16]  As such, it is a conservative fragment, just like classical logic and unlike linear or intuitionistic logics. This is no surprise because, just like CoL, IF logic is a semantically conceived logic.

In fact, for a long time, IF logic remained a pure semantics without a syntax. In its full first-order language, IF logic was simply known to be unaxiomatizable. As for the propositional fragment, there was none because the traditional approaches to IF logic had failed to offer any non-classical semantics for propositional connectives.  Under CoL’s cirquent-based approach to IF logic this is no longer so, and “independence-friendly” propositional connectives are just as meaningful as their quantifier counterparts. Based on this new treatment, a sound and complete axiomatization for propositional IF logic has been later found.[Xu14, Xu16] 


1.7 The ‘from semantics to syntax’ paradigm

CoL’s favorite ‘from semantics to syntax’ paradigm for developing a logic can be characterized as consisting of three main stages. The first one can be called the Informal semantics stage, at which the main intuitions are elaborated along with the underlying motivations, and the formal language of the logic is agreed upon.  The second one is the Formal semantics stage, at which those intuitions are formalized as a mathematically strict semantics for the adopted language, and definitions of truth and validity are given. Finally, the third one is the Syntax stage, at which one constructs axiomatizations for the corresponding set of valid principles,   whether in the full language of the logic or some natural fragments of it, and proves the adequacy (soundness and completeness) of such constructions. 

Figure 1.7.1: Three stages of developing a logic

CoL and classical logic went through all three stages in sequence. So did IF logic, even though for a long time it was stuck at the second stage. As for linear and intuitionistic logics, they essentially jumped from the first stage directly to the third stage, skipping the inermediary stage. It is the absence of formal rather than informal semantics that we meant when saying that the two logics were conceived syntactically rather than semantically. Why is such a jump wrong? It is impossible to directly “prove” that the proposed syntax adequately corresponds to the informal-semantical intuitions underlying the logic. After all, Syntax is mathematically well defined while Informal semantics is from the realm of philosophy or intuitions, so an adequacy claim lacks any mathematical meaning. Of course, the same is the case with Formal semantics vs. Informal semantics. But, at least, both are “semantics”, which makes it qualitatively easier to convincingly argue (albeit not prove) that one adequately corresponds to the other. Once such a correspondence claim is accepted, one can prove the adequacy of the syntax by showing that it is sound and complete with respect to the formal semantics. 

The intermediary role of Formal semantics can be compared with that of Turing machines.  Since the intuitive concept of a machine (algorithm) and the mathematical concept of a Turing machine are both about “machines”, it is relatively easy to argue in favor of the (mathematically unprovable) Church-Turing thesis, which claims an adequate correspondence between the two. Once this thesis is accepted, one can relatively easily show --- this time mathematically --- that recursive functions or lambda calculus, too, adequately correspond to our intuitions of machine-computability. Arguing in favor of such a claim directly, without having the intermediary Turing machine model, would not be easy, as recursive definitions or lambda terms do not at all resemble what our intuition perceives as machines.

Based directly on the resource intuitions associated with linear logic, can anyone tell whether, for instance, the principle P  (P  PP)  P should be accepted? An orthodox linear logician might say ‘No, because it is not provable in Girard’s canonical system’. But the whole point is that we are just trying to understand what should be provable and what should not. From similar circularity suffer the popular attempts to “semantically” justify intuitionistic provability in terms of … intuitionistic provability.



2 Games


2.1 The two players

The CoL games are between two players, called Machine and Environment (not always capitalized, and may take articles). On the picture below we see a few other names for these players.

We will be using  and   as symbolic names for Machine and Environment, respectively.  is a deterministic mechanical device only capable of following algorithmic strategies.  ’s strategies, on the other hand, are arbitrary. Throughout this page, we shall consistently use the green color to represent Machine, and red for Environment. As seen from the picture, our sympathies are with the machine. Why should we be fans of the machine even when it is us who act in the role of its “evil” environment? Because the machine is a tool, and what makes it valuable as such is exactly its being a good player. In fact, losing a game by the machine means that it is malfunctioning.   Imagine Bob using a computer for computing the “28% of x” function in the process of preparing his US federal tax return. This is a game where the first move is by Bob, consisting in inputting a number m and meaning asking his machine the question “what is 28% of m?”. The machine wins iff it answers by the move/output n such that n=0.28m. Of course, Bob does not want the machine to tell him that 27,000 is 28% of 100,000. In other words, he does not want to win against the machine. For then he could lose the more important game against Uncle Sam.


2.2 Moves, runs and positions

Machine and Environment interact with each other through mutually observable actions.  We will be using the term “move” instead of “action”. Looking back at the ordinary Turing machine model, it is about games where only two moves are made: the first move, called “input”, is by the environment, and the second move, called “output”, is by the machine.   

We agree on the following:

·       A move is any finite string over the keyboard alphabet. We will be using a,b,g  as metavariables for moves.

·       A colored move is a move a together with one of the two colors green or red, with the color indicating which player has made the move. We shall write such a move as a or a, depending on its color (in black-and-white presentations, a and a will be written instead). Often we omit the word “colored” and simply say “move”.  The letter l will be used as a metavariable for colored moves.

·        A run is a (finite or infinite)  sequence of colored moves. We will be using G,D  as metavariables for runs.

·        A position is a finite run. We will be using F,Y,X,W as metavariables for positions.

·       We will be writing runs and positions as  áa,β, gñ,  áFñ,  áF, Y,β, Gñ,   etc.  The meanings of such expressions should be clear. For instance, áF, Y,β, Gñ is the run consisting of the (colored) moves of the position F, followed by the moves of the position Y, followed by the move β, and then by the moves of the (possibly infinite) run G.

·       á ñ thus stands for the empty position.


2.3 Constant games

A gamestructure is a nonempty set Lr of positions, called legal positions, such that, whenever a position is in Lr, so are all initial segments of it.  The empty position á ñ is thus always legal. We extend gamestructures to include infinite runs as well, by stipulating that an infinite run G is in Lr iff so is every finite initial segment of G.  Intuitively, Lr is the set of legal runs. The runs that are not in Lr are illegal. An illegal move in a given position áFñ is a move l such that áF,lñ is illegal. The player who made the first illegal move in a given run is said to be the offender. Intuitively, illegal moves can be thought of as moves that cannot or should not be made. Alternatively, they can be seen as actions that cause the system crash (e.g., requesting to divide a number by 0).

Gamestructures can be visualized as upside-down trees where the nodes represent positions. Each edge is labeled with a colored move. Such an edge stands for a legal move in the position represented by the upper node of it. Here is an example:  

Figure 2.3.1: A gamestructure

This gamestructure consists of the following 16 runs: á ñ,   áañ,  áβñ,   ágñ,  áa,βñ,  áa, gñ,  áβ,añ,  ág, añ,  ág,βñ,  ág, gñ,  áa, g,βñ,   áa, g,gñ,  ág, a,βñ,  ág, a, gñ,  ág, β, añ,  ág, g,añ.  All of the infinitely (in fact, uncountably) many other runs are illegal. An example of an illegal run is ág, g,β, β, añ. The offender in it is Environment, because the offending third move is red. 

Let Lr be a gamestructure. A content on Lr is a function Wn: Lr  {,}.  When WnáΓñ = , we say that Γ is won by the machine (and lost by the environment); and when WnáΓñ =, we say that Γ is won by the environment (and lost by the machine). We extend the domain of Wn to all runs by stipulating that an illegal run is always lost by the offender. Since we are fans of Machine, the default meaning of just “won” (or “lost”) is “won (or lost) by the machine”.

Definition 2.3.2 A constant game G is a pair (LrG,WnG), where LrG is a gamestructure, and WnG is a content on LrG.

Figure 2.3.3 below shows a constant game of the structure of Figure 2.3.1:

Figure 2.3.3: A constant game

Here the winner in each position is indicated by the color of the corresponding node. So, for instance, the run ág,a, βñ is won by the machine; but if this run had stopped after its second move, then the environment would be the winner.  Of course, such a way of indicating winners is not sufficient if there are infinitely long branches (legal runs), for such branches do not have “the corresponding nodes”.

We say that a constant game is strict iff, in every legal position, at most one of the two players has legal moves. Our games generally are not strict. For instance, in the start position of the game of Figure 2.3.3, both players have legal moves. We call such (not-necessarily-strict) games free. Free games model real-life situations more directly and naturally than strict games do. Hardly many tasks that humans, computers or robots perform are strict. Imagine you are playing chess over the Internet on two boards against two independent adversaries that, together, form the (one) environment for you. Let us say you play white on both boards. Certainly in the initial position of this game only you have legal moves. However, once you make your first move --- say, on board #1 --- the picture changes. Now both you and the environment have legal moves, and who will be the next to move depends on who can or wants to act sooner. Namely, you are free to make another opening move on board #2, while the environment --- adversary #1 --- can make a reply move on board #1. A strict-game approach would have to impose some not-very-adequate supplemental conditions uniquely determining the next player to move, such as not allowing you to move again until receiving a response to your previous move. Let alone that this is not how the real two-board game would proceed, such regulations defeat the very purpose of the idea of parallel/distributed computations with all the known benefits it offers.

Because our games are free, strategies for them cannot be defined as functions from positions to moves, because, in some positions (such as the root position in the game of Figure 2.3.3) both players may have legal moves and, if both are willing to move, which of them acts sooner will determine what will be the next move.

The exact meaning of “strategy” will be defined later, but whatever it means, we can see that the machine has a winning strategy in the game of Figure 2.3.3, which can be put this way:     Regardless of what the adversary is doing or has done, go ahead and make move α; make β as your second move if and when you see that the adversary has made move γ, no matter whether this happened before or after your first move”.  This strategy obviously guarantees that the machine will not offend. There are 5 possible legal runs  consistent with it, i.e., legal runs that could be generated when it is followed by the machine: áañ,  áa, βñ,  áβ, añ,   áa, g,βñ  and ág,a,βñ. All are won by the machine.

Let G be a constant game. G is said to be finite-depth iff there is a (smallest) integer d, called the depth of G, such that the length of every legal run of G is £d. And G is perifinite-depth iff every legal run of it is finite, even if there are arbitrarily long legal runs. Let us call a legal run Γ of G maximal iff Γ is not a proper initial segment of any other legal run of G. Then we say that G is finite-breadth iff the total number of maximal legal runs of G, called the breadth of G, is finite. Note that, in a general case, the breadth of a game may be not only infinite, but even uncountable. G is said to be (simply) finite iff it only has a finite number of legal runs. Of course, G is finite only if it is finite-breadth, and when G is finite-breadth, it is finite iff it is finite-depth iff it is perifinite-depth. 

As noted in Section 2.2, computational problems in the traditional sense are nothing but functions (to be computed). Such problems can be seen as the following types of depth-2 games:

Figure 2.3.4: The “successor” game

·       Why is the root green here?  Because it corresponds to the situation where there was no input. The machine has nothing to answer for, so it wins.

·       Why are the 2nd level nodes red? Because they correspond to situations where there was an input but no output was generated by the machine. So the machine loses.

·       Why does each group of 3rd level nodes has exactly one green node? Because a function has exactly one (“correct”) value for each argument.

·       What particular function is this game about? The successor function: f(n)=n+1.

Once we agree that computational problems are nothing but games, the difference in the degrees of generality and flexibility between the traditional approach to computational problems and our approach becomes apparent and appreciable. What we see in Figure 2.3.4 is indeed a very special sort of games, and there is no good call for confining ourselves to its limits. In fact, staying within those limits would seriously retard any more or less advanced and systematic study of computability.

First of all, one would want to get rid of the “one green node per sibling group” restriction for the third-level nodes. Many natural problems, such as the problem of finding a prime integer between n and 2n, or finding an integral root of x2-2n=0, may have more than one as well as less than one solution. That is, there can be more than one as well as less than one “right” output on a given input n.

And why not further get rid of any remaining restrictions on the colors of whatever-level nodes and whatever-level arcs.  One can easily think of natural situations where, say, some inputs do not obligate the machine to generate an output and thus the corresponding 2nd level nodes should be green. An example would be the case where the machine is computing a partially-defined function f and receives an input n on which f is undefined.

So far we have been talking about generalizations within the depth-2 restriction, corresponding to viewing computational problems as very short dialogues between the machine and its environment. Permitting longer-than-2 or even infinitely long runs would allow us to capture problems with arbitrarily high degrees of interactivity and arbitrarily complex interaction protocols.  The task performed by a network server is an example of an infinite dialogue between the server and its environment --- the collection of clients, or let us just say the rest of the network.

It also makes sense to consider “dialogues” of lengths less than 2. “Dialogues” of length 0, i.e. games of depth 0 are said to be elementary. There are exactly two elementary constant games, denoted by  and :

Note that the symbols  and  thus have dual meanings: they may stand for the two elementary games as above, or for the corresponding two players. It will usually be clear from the context which of these two meanings we have in mind.

Just like classical logic, CoL sees no extensional distinction between “snow is white” and , or between “snow is black” and : All true propositions, as games, are , and all false propositions are . In other words, a proposition is a game automatically won by the machine when true and lost when false. This way, CoL’s concept of a constant game is a generalization of the classical concept of a proposition.


2.4 Not-necessarily-constant games

We fix an infinite set Variables = {var0, var1, var2,… } of variables. As usual, lowercase letters near the end of the Latin alphabet will be used to stand (as metavariables) for variables. We further fix the set Constants = {0,1,2,3,…} of decimal numerals, and call its elements constants. With some abuse of concepts, we shall often identify constants with the numbers they represent.

A universe (of discourse) is a pair U = (Dm, Dn), where Dm, called the domain of U, is a nonempty set, and Dn, called the denotation function of U,  is a (total) function of type Constants ® Dm.  The elements of Dm will be referred to as the individuals of U. The intuitive meaning of d=Dn(c) is that the individual d is the denotat of the constant c and thus c is a name (or code) of d. So, the function Nm from Dm to the powerset of Constants satisfying the condition cÎNm(d) Û d=Dn(c) can be called the naming function of U. Of course, whenever convenient, a universe can be characterized in terms of its naming function rather than denotation function. 

A universe (Dm, Dn) is said to be ideal iff Dn is a bijection. Generally, in a not-necessarily-ideal universe, some individuals may have unique names, some have many names, and some have no names at all. Real-world universes are seldom ideal: not all people living or staying in the United States have social security numbers;  most stars and planets of the Galaxy have no names at all, while some  have several names (Morning Star = Evening Star = Venus); etc. A natural example of an inherently non-ideal universe from the world of mathematics would be the one whose domain is the set  of real numbers, only some of whose elements have names, such as 5, 1/3, Ö2 or p. Generally, even if the set of constants was not fixed, no universe with an uncountable domain would be “ideal  for the simple reason that  there can only be countably many names. This is so because names, by their very nature and purpose, have to be finite objects. Observe also that many properties of common interest, such as computability or decidability, are usually sensitive with respect to how objects (individuals) are named, as they deal with the names of those objects rather than the objects themselves. For instance, strictly speaking, computing a function f(x) means the ability to tell, after seeing a (the) name of an arbitrary object a, to produce a (the) name of the object b with b=f(a).  Similarly, an algorithm that decides a predicate p(x) on a set S, strictly speaking, takes not elements of S --- which may be abstract objects such as numbers or graphs --- but rather names of those elements, such as decimal numerals or codes. It is not hard to come up with a nonstandard naming of the natural numbers through decimal numerals where the predicate “x is even” is undecidable.  On the other hand, for any undecidable arithmetical predicate p(x), one can come up with a naming  such that p(x) becomes decidable --- for instance, one that assigns even-length names to all a with p(a) and assigns odd-length names to all a with ¬p(a). Classical logic exclusively deals with individuals of a universe without a need to also consider names for them, as it is not concerned with decidability or computability. CoL, on the other hand, with its computational semantics, inherently calls for being more careful about differentiating between individuals and their names, and hence for explicitly considering universes in the form (Dm, Dn) rather than just Dm as classical logic does. 

Where Vr is a set of variables and Dm is the domain of some universe, by a Vr®Dm  valuation we mean a (total) function e of type Vr®Dm. When Vr and Dm are clear from the context, we may omit an explicit reference to them and simply say “valuation”. References to a universe U or its components can be similarly omitted when talking about individuals, denotats, names or some later-defined concepts such as those of a game or a function.

Definition 2.4.1 Let n be a natural number. An n-ary game is a tuple G=(DmG,DnG,VrG,MpG), where (DmG,DnG) is a universe, VrG is a set of n distinct variables, and MpG is a mapping of VrG®DmG valuations to constant games. 

We refer to the elements of VrG as the variables on which the game G depends.  We further refer to the pair (DmG,DnG) as the universe of G, and denote it by UnG. Correspondingly, a game sometimes can be written as the triple (UnG,VrG,MpG) rather than quadruple (DmG,DnG,VrG,MpG). We further refer to DmG as the domain of G, refer to DnG as the denotation function of G, and refer to VrG®DmG valuations as G-valuations.

In classical logic, under an intensional (variable-sensitive) understanding, the definition of the concept of an n-ary predicate would look exactly like our definition of an n-ary game after omitting the (now redundant) Dn component, with the only difference that there the Mp function returns propositions rather than constant games. And, just like propositions are nothing but 0-ary predicates, constant games are nothing but 0-ary games. Thus, games generalize constant games in the same way as predicates generalize propositions. And, as constant games are generalized propositions, games are generalized predicates.

In formal contexts, we choose a similar intensional approach to functions. The definition of a function f below is literally the same as our definition of a game G, with the only difference that Mpf is now a mapping of Vrf®Dmf valuations to Dmf (rather than to constant games).  

 Definition 2.4.2 Let n be a natural number. An n-ary function is a triple f=(Dmf, Dnf Vrf,Mpf), where (DmG,DnG) is a universe, Vrf is a set of n distinct variables, and Mpf is a mapping of Vrf®Dmf valuations to Dmf. 

Just like in the case of games, we refer to the elements of Vrf as the variables on which the function f depends, refer to Dmf as the domain of f, etc.

Let U be a universe, c a constant and x a variable. We shall write cU to mean the function f with Unf=U, Vrf=Æ and with Mpf such that, for (the only) f-valuation e,   Mpf(e)=DnU(c). And we shall write xU to mean the function f with Unf=U, Vrf={x} and with Mpf such that, for any f-valuation e, Mpf(e)=e[x].

Given a game G and an X®DmG valuation e with VrGÍX, we write e[G] to denote the constant game MpG(eʹ) to which MpG maps eʹ, where  eʹ is the restriction of e to VrG (i.e.,  the G-valuation that agrees with e on all variables from VrG). Such a constant game e[G] is said to be an instance of G.  Also, for readability, we usually write LreG and WneG instead of Lre[G]  and  Wne[G].  Similarly, given a function f and an X®Dmf valuation e with VrfÍX, we write e[f] to denote the individual Mpf(eʹ) to which Mpf maps eʹ, where  eʹ is the restriction of e to Vrf.

We say that a game is elementary iff so are all of its instances. Thus, games generalize elementary games in the same sense as constant games generalize  and . Further, since the “legal run” component of all instances of elementary games is trivial (the empty run á ñ is the only legal run), and since depending on runs is the only thing that differentiates constant games from propositions, we can and will use “predicate” and “elementary game” as synonyms. Specifically, we understand a predicate p as the elementary game G which depends on the same variables as p such that, for any valuation e, WneGá ñ= iff p is true at e. And vice versa: An elementary game G will be understood as the predicate p which depends on the same variables as G and which is true at a given valuation e iff WneGá ñ= .  

Convention 2.4.3 Assume F is a function (resp. game). Following the standard readability-improving practice established in the literature for functions and predicates, we may fix a tuple (x1,…,xn) of pairwise distinct variables for F when first mentioning it, and write  F as F(x1,…,xn). When doing so, we do not necessarily mean that {x1,…,xn}=VrF. Representing F as F(x1,…,xn) sets a context in which, where g1,…,gn are functions with the same universe as F, we can write F(g1,…,gn) to mean the function (resp. game) H with UnH=UnF, VrH=(VrH –{x1,…,xn})ÈVrg1 ÈÈ Vrgn  and with MpH such that the following condition is satisfied:

·       For any H-valuation e, e[H]=eʹ[F], where eʹ is the F-valuation with eʹ[x1]=e[g1], …, eʹ[xn]=e[gn].

Further, we allow for any of the above “functions” gi to be just a constant c or just a variable x. In such a case, gi should be correspondingly understood as the 0-ary function cU or the unary function xU, where U=UnF. So, for instance, F(0,x) is our lazy way to write F(0F,xU).

The entities that in common language we call games are at least as often non-constant as constant. Board games such as chess and checkers are examples of constant games. On the other hand, almost all card games are more naturally represented as non-constant games: each session/instance of such a game is set by a particular permutation of the card deck, and thus the game can be understood as a game that depends on a variable x ranging over the possible settings of the deck. Even the game of checkers has a natural non-constant generalization Checkers(x) with x ranging over positive even integers, meaning a play on the board of size x×x where, in the initial position, the first 1.5x black cells are filled with white pieces and the last 1.5x black cells with black pieces.  Then the ordinary checkers can be written as Checkers(8). Furthermore, the numbers of pieces of either color also can be made variable, getting an even more general game Checkers(x,y,z), with the ordinary checkers being the instance Checkers(8,12,12) of it. By allowing rectangular-shape boards, we would get a game that depends on four variables, etc. Computability theory also often appeals to non-constant games to illustrate certain complexity-theory concepts such as alternating computation or PSPACE-completeness. The so called Formula Game or Generalized Geography are typical examples. Both can be understood as games that depend on a variable x, with x ranging over quantified Boolean formulas in Formula Game and over directed graphs in Generalized Geography.

Consider a game G.  What we call a unilegal run of G is a run which is a legal run of all instances of G. And we say that G is unistructural iff all legal runs of all of its instances are unilegal. The class of unistructural games is known to be closed under all of the game operations studies in CoL.[Jap03]  While natural examples of non-unistructural games exist such as the games mentioned in the above paragraph, virtually all of the other examples of particular games discussed elsewhere on the present site are unistructural.

Non-constant games, as long as they are unistructural, can be visualized as trees in the earlier seen style, with the difference that the nodes of the tree can now be labeled with any predicates rather than only propositions (colors) as before. For any given valuation e, each such label L is telling us the color of the node. Namely, the L-labeled node is green if L is true at e, and red if L is false. 

Figure 2.3.5: The “generalized successor” game

This is a game which depends on x. Specifically, for every valuation e, the game is about computing the function fe, defined by fe (n) = n+e(x) (“the xth successor of n”).  Note that we have different functions and thus different constant games for different valuations e here.

Denoting the game of Figure 2.3.5 by G(x), the game of Figure 2.3.4 can be seen to be the instance G(1) of it. The latter results from replacing x by 1 in Figure 2.3.5. This replacement turns every label m=n+x into the proposition m=n+1, i.e., into  (green filling) or  (red filling).


2.5 Static games

In the particular games that we have seen so far or will see in the subsequent sections, when talking about the existence of a winning strategy or the absence of thereof, the question about the (relative) speeds of the players was never relevant. That is because all those games shared one nice property, called the static property. Below are some intuitive characterizations of this important class of games.

        Static games are games where the speed of the adversary is not an issue: if a player has a winning strategy, the strategy will remain good no matter how fast its adversary is in making moves. And if a player does not have a winning strategy, it cannot succeed no matter how slow the adversary is. 

        Static games are games where “it never hurts a player to postpone making moves” (Blass’ words from his AMS review of [Jap03]).

        Static games are contests of intellect rather than speed. In such games, what matters is what to do (strategy) rather than how fast to do (speed).

The games that are not static we call dynamic. The following games are dynamic: 

In either game, the player who is quick enough to make the first move becomes the winner. And asking whether Machine has a winning strategy is not really meaningful: whether Machine can win or not depends on the relative speeds of the two players. In a sense, B is even “worse” than A. Just as in A, it would not be a good idea for Machine to wait, because, unless Environment is stupid enough to also decide to wait, Machine will lose. Let us now say that Machine goes ahead and initiates the first move. What may happen in B is that Environment moves before Machine actually completes its move. This will make Machine not only the loser but also the offender. Machine cannot even be sure that its move will be legal!  If communication happens by exchanging messages through a (typically) asynchronous network, that often has some unpredictable delays, this can also be a contest of luck: assuming that the arbitration is done by Environment or a third party who is recording the order of moves, it is possible that Machine makes a move earlier than Environment does, but the message carrying that move is delivered to the  arbiter only after Environment’s move arrives, and the arbiter will be unable to see that it was Machine who moved first. An engineering-style attempt to neutralize this problem could be to let all moves carry timestamps. But this would not save the case: even though timestamps would correctly show the real order of moves by each particular player, they could not be used to compare two moves by two different players, for the clocks of the two players would never be perfectly synchronized.

Another attempt to deal with problems in the above style could be to assign to each player, in a strictly alternating order, a constant-length time slot during which the player has exclusive access to the communication medium. Let alone that this could introduce some unfair asymmetry in favor of the player who gets the first slot, the essence of the problem would still not be taken care of: some games would still essentially depend on the relative speeds of the two players, even if arguably no longer on the speed of the network.

Formally, the concept of static games is defined in terms of “delays”. We say that run Δ is a green (resp. red) delay of run Γ iff the following two conditions are satisfied:

1.     The moves of either color are arranged in Γ in the same order as in Δ.

2.     For any n,k³1, if the kth  red (resp. green) move is  made earlier than the the nth green (resp. red)  move in Γ, then so is it in Δ.

In other words, Δ is the result of shifting to the right (“delaying”) some green (resp. red) moves in Γ without violating their order. Example: á0,2,1,3,4,5,7,8,6,10,9ñ is a green delay of á0,1,2,3,4,5,6,7,8,9,10ñ.  The former is obtained from the latter by shifting to the right some green moves. When doing so, a green move can jump over a red move, but one green move cannot jump over another green move.

Now, we say that a constant game G is static iff, for either player (color) P and any runs Γ and Δ such that Δ is a P delay of Γ, in the context of G, the following two conditions are satisfied:

1.     If Γ is won by P, then so isΔ.

2.     If P does not offend in Γ, then neither does it in Δ.

This concept extends to all games by stipulating that a not-necessarily-constant game is static iff so are all of its instances.

All game operations studied in CoL have been shown to preserve the static property of games.[Jap03]  So, as long as the atoms of an expression represent static games, so does the whole expression. One natural subset of all static games is the closure of elementary games under the operations of CoL.

As already noted, CoL restricts its attention to static games only (at least, at its present stage of development). To see why static games are really what CoL is willing to call “pure” computational problems, imagine a play over the delay-prone Internet. If there is a central arbiter (which can be located either in one of the players' computer or somewhere on a third, neutral territory) recording the order of moves, then the players have full access to information about the official version of the run that is being generated, even though they could suffer from their moves being delivered with delays. But let us make the situation even more dramatic: assume, as this is a typical case in distributed systems, that there is no central arbiter. Rather, each players’ machine records moves in the order it receives them, so that we have what is called distributed arbitration. Every time a player makes a move, the move is appended to the player’s internal record of the run and, at the same time, mailed to the adversary. And every time a message from the adversary arrives, the move contained in it is appended to the player’s record of the run. The game starts. Seeing no messages from Environment, Machine decides to go ahead and make an opening moveα. As it happens, Environment also decides to make an “opening” move β. The messages carryingαandβcross. So, after they are both delivered, Machine’s internal records show the position áa,bñ, while Environment thinks that the current position is áb,añ. Both of the players decide to make two consecutive new moves: g,d and e,w, respectively, and the two pairs of messages, again, cross. 

After making their second series of moves and receiving a second series of “replies” from their adversaries, both players decide to make no further moves. The game thus ends. According to Machine’s records, the run was áa,b,g,d,e,wñ,  while Environment thinks that the run was áb,a,e,w,g,dñ.  As for the “real run”, i.e. the real order in which these six moves were made (if this concept makes sense at all), it can be yet something different, such as, say,  áb,a,g,e,d,wñ. A little thought can convince us that in any case the real run, as well as the version of the run seen by Environment, will be a green delay of the version of the run seen by Machine. Similarly, the real run, as well as the version of the run seen by Machine, will be a red delay of the version of the run seen by Environment. Hence, provided that the game is static, either player can fully trust its own version of the run and only care about making good moves for this version, because regardless of whether it shows the true or a distorted picture of the real run, the latter is guaranteed to be successful as long as the former is.  Moreover: for similar reasons, the player will remain equally successful if, instead of immediately appending the adversary's moves to its own version of the run, it simply queues those moves in a buffer as if they had not arrived yet, and fetches them only later at a more convenient time, after perhaps making and appending to its records some of its own moves first. The effect will amount to having full control over the speed of the adversary, thus allowing the player to select its own pace for the play and worry only about what moves to make rather than how quickly to make them.

Thus, static games allow players to make a full abstraction from any specific assumptions regarding the type of arbitration (central or distributed), the speed of the communication network and the speed of the adversary: whatever strategy they follow, it is always safe to assume or pretend that the arbitration is fair and unique (central), the network is perfectly accurate (zero delays) and the adversary is “slow enough”.  On the other hand, with some additional thought, we can see that if a game is not static, there will always be situations when no particular one of the above three sorts of abstractions can be made. Specifically, such situations will emerge every time when a player P’s strategy generates a P-won run that has some P-lost P-delays.




3 The CoL zoo of game operations

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.


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)

 (branching),   (parallel),   (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 intuitive explanations as well as formal definitions of all of the above-listed operators. We agree that throughout those definitions, F ranges over positions, and G over runs. Each such definition has two clauses, one telling us when a position is a legal position of the compound game, and the other telling us who wins any given legal run. The run G seen in the second clause of the definition is always implicitly assumed to be a legal legal run of the game that is being defined.


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 ideal 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, 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). They also preserve the property of being unistructural in x (for whatever variable x).


3.2 Prefixation

Unlike the operators listed in the preceding subsection, the operation of prefixation is not meant 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 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 G with UnG=UnA, VrG=VrA and with MpG such that, for any G-valuation e, we have:

·       LreG={Φ |  áΨ,ΦñÎLreA};

·       WneG áGñ = WneA áΨ,Gñ.

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.2.1  Assume A is a game.  A is defined as the game G with UnG=UnA, VrG=VrA and with MpG such that, for any G-valuation e, we have:

·       LreG={Φ: ΦÎLreA};

·       WneG áGñ =   iff   WneA áGñ = .

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.2.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.2.2 to see that this is indeed so.


3.4 Choice operations

Choice conjunction (“chand”)  and choice disjunction (“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 A0 and A1 are games with a common universe U.

a)     A0  A1 is defined as the game G with UnG=U,  VrG=VrA0ÈVrA1  and with MpG such that, for any G-valuation e, we have:

·       LreG={á ñ} È {ái,Φñ: iÎ{0,1}, ΦÎLreAi};

·       WneG á ñ = ;  WneG ái,Gñ = WneAi áGñ.

b)     A0  A1 is defined as the game G with UnG=U, VrG=VrA0ÈVrA1  and with MpG such that, for any G-valuation e, we have:

·       LrG={á ñ} È {ái,Φñ: iÎ{0,1}, ΦÎLrAi};

·       WnG á ñ = ;  WnG ái,Gñ = WnAi áGñ.

The game A of Figure 3.2.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 (“chall”)  xA(x) of it is nothing but the “infinite choice conjunction” A(0)A(1)A(2) …,  and the choice existential quantification (“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 all choice operations.

Definition 3.4.2 Assume x is a variable and A=A(x) is a game.

a)     xA(x)  is defined as the game G with UnG=UnA, VrG=VrA-{x}  and with MpG such that, for any G-valuation e, we have:

·       LreG={á ñ} È {ác,Φñ: cÎConstants, ΦÎLreA(c)};

·       WneG á ñ = ;  WneG ác,Gñ = WneA(c)áGñ.

b)     xA(x)  is defined as the game G with UnG=UnA, VrG=VrA-{x}  and with MpG such that, for any G-valuation e, we have:

·       LreG={á ñ} È {ác,Φñ: cÎConstants, ΦÎLreA(c)};

·       WneG á ñ = ;  WneG ác,Gñ = WneA(c)áGñ.

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 xyA(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 computability logic are constructive. Computability (“truth”) of  xyA(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.

Similarly, let Halts(x,y) be the predicate “Turing machine x halts on input y”. Consider xy(Halts(x,y)  Halts(x,y)).    It is true in classical logic, yet not in a constructive sense. Its truth means that, for all x and y, either Halts(x,y)  or Halts(x,y) is true, but it does not imply existence of an actual way to tell which of these two is true after all. And such a way does not really exist, as the halting problem is undecidable. This means that xy(Halts(x,y)  Halts(x,y)) is not computable. Generally, as pointed out earlier, the principle of the excluded middle  A OR A”, validated by classical logic and causing the indignation of the constructivistically-minded, is not valid in computability logic with OR understood as choice disjunction. The following is an example of a constant game of the form A  A with no algorithmic solution (why, by the way?):

 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 (“pand”) AB and the parallel disjunction (“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.’. 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 G and string a,  G a means  the result of removing from G all moves except those of the form ab,  and then deleting the prefix ‘a’ 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 G is the leftmost branch of the tree for (  ) (  ) shown in Figure 3.5.3, we have G0. =  á1ñ and G1. = á1ñ. Intuitively, we see this G as consisting of two subruns, one (G0.) being a run in the first -disjunct of (  ) (  ) , and the other (G1.) being a run in the second disjunct.

Definition 3.5.2 Assume A0 and A1 are games with a common universe U.

a)     A0A1 is defined as the game G with UnG=U, VrG=VrA0ÈVrA1  and with MpG such that, for any G-valuation e, we have:

·       FÎ LreG iff every move of F has the prefix ‘0.’ or ‘1.’ and,  for both iÎ{0,1},  Fi.Î LreAi;

·       WneG áGñ =  iff, for both iÎ{0,1},  WneAi áGi.ñ=.

b)     A0A1 is defined as the game G with UnG=U, VrG=VrA0ÈVrA1  and with MpG such that, for any G-valuation e, we have:

·       FÎ LreG iff every move of F has the prefix ‘0.’ or ‘1.’ and,  for both iÎ{0,1},  Fi. Î LreAi;

·       WneG áGñ= iff, for both iÎ{0,1},  WneAi áGi.ñ=.

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: Por-ing two games


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 F of A as the game  áFñ 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 G= á1.7, 0.7, 0.49, 1.49ñ  of game A = xy(yx2)   xy(y=x2) induces the following sequence, showing how things evolve as G runs, i.e., how the moves of G affect/modify the game that is being  played:



xy(yx2)  xy(y=x2)    i.e. A

xy(yx2)  y(y=72)        i.e. á1.7ñA

y(y72)  y(y=72)            i.e. á1.7,0.7ñA

4972  y(y=72)                 i.e. á1.7,0.7,0.49ñA

4972  49=72                      i.e. á1.7,0.7,0.49,1.49ñA


The run hits the true proposition 4972  49=72, 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 x is a variable and A=A(x) is a game.

a)     xA(x) is defined as the game G with UnG=UnA, VrG=VrA-{x}  and with MpG such that, for any G-valuation e, we have:

·       ΦÎ LreG iff every move of Φ has the prefix ‘c.’ for some cÎConstants and, for all such c, Φc. Î LreA(c);

·       WneG áGñ =  iff, for all cÎConstants, WneAáGc.ñ=.

b)     xA(x) is defined as the game G with UnG=UnA, VrG=VrA-{x}  and with MpG such that, for any G-valuation e, we have:

·       ΦÎ LreG iff every move of Φhas the prefix ‘c.’ for some cÎConstants and, for all such c, Φc. Î LreA(c);

·       WneG áGñ= iff, for all cÎConstants, WneAáGc.ñ=.


The remaining 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 is a game.

a)     A is defined as the game G with UnG=UnA, VrG=VrA  and with MpG such that, for any G-valuation e, we have:

·       ΦÎ LreG iff every move of Φ has the prefix ‘c.’ for some cÎConstants   and, for all such c, Φc. Î LreA;

·       WneG áGñ =  iff, for all cÎConstants, WneAáGc.ñ=.

b)     A is defined as the game G with UnG=UnA, VrG=VrA  and with MpG such that, for any G-valuation e, we have

·       ΦÎ LreG iff every move of Φ has the prefix ‘c.’ for some cÎConstants   and, for all such c, Φc. Î LreA;

·       WneG áGñ =  iff, for all cÎConstants, WneAáGc.ñ=.

As was the case with choice operations, we can see that the definition of each of the above parallel operations 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)= A B,  (A B)=  A B,  xA(x)=x A(x),  xA(x)=x A(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  (A B) and  A=  A. Two more parallel operations defined in terms of negation and other parallel operations are parallel implication (“pimplication”) and parallel rimplication (“primplication”). In the latter, the prefix “r” added to “implication” stands for “recurrence”. 

Definition 3.5.7    a) A0  A1  =def