Giorgi Japaridze's page for

**Computability Logic**

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

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

可计算性逻辑

(CoL)

** NOTE**: This site should be viewed with

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!

**Contents**

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.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.6
Reduction

3.10 Toggling operations

3.11 Cirquents

5 The
language of CoL and its semantics

5.1 Formulas

5.2 Interpretations

5.3 Validity

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.6 Clarithmetics for provable computability

8 CoL-based
knowledgebase and resourcebase systems

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

**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*; *situation*s 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.

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* *P**P*) *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.28*m*. 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

· 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

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

**Definition
2.3.2** A *constant game**G* is a pair **(Lr**^{G}**,Wn**^{G}**)**, where **Lr**^{G}**
**is a gamestructure, and **Wn*** ^{G}*
is a content on

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

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

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 2^{nd}
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 3^{rd} 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 2*n*, or finding an
integral root of *x*^{2}-2*n*=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 2^{nd} 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* = {*var*_{0}, *var*_{1},
*var*_{2},… }
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

A ** universe** (of
discourse) is a pair

A universe (**Dm**,
**Dn**) is said to be *ideal*** **iff

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

**Definition**** 2.4.1 **Let *n* be a natural number. An *n*-ary ** game** is a tuple

We refer to the elements of **Vr*** ^{G}* as the
variables on which the game

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 **Mp*** ^{f}*
is now a mapping of

**Definition
2.4.2 **Let *n* be a natural
number. An *n*-ary ** function** is a triple

Just like in the case of games, we refer to the
elements of **Vr*** ^{f}* as the variables on which the function

Let *U* be a
universe, *c* a constant and *x* a variable. We shall write *c ^{U}* to mean the function

Given a game *G*
and an *X*®**Dm*** ^{G}* valuation

We say that a game is *eleme*** ntary**
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

**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 (*x*_{1},…,*x*_{n}) of
pairwise distinct variables for *F*
when first mentioning it, and write
*F* as *F*(*x*_{1},…,*x*_{n}). When doing so, we do not necessarily mean that {*x*_{1},…,*x*_{n}}=**Vr*** ^{F}*.
Representing

· For any *H*-valuation
*e*, *e*[*H*]=*e*ʹ[*F*], where *e*ʹ is the *F*-valuation with *e*ʹ[*x*_{1}]=*e*[*g*_{1}], …, *e*ʹ[*x*_{n}]=*e*[*g*_{n}].

Further, we allow
for any of the above “functions” *g _{i}*
to be just a constant

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.5*x* black cells are filled with white
pieces and the last 1.5*x* 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

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* f _{e}*,
defined by

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.

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

2. For any *n*,*k*³1, if the *k*th red (resp. green) move is made earlier than the the *n*th 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)

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.

*Negation: *

** Conjunctions: ** (

** Disjunctions: ** (

*Recurrences: *** **(

** Corecurrences:** (

*Universal
quantifiers:** *** **(

*Existential quantifiers:*** **(

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

** Rimplications:** (

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 *A**B*, 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* *B**C* should be
understood as *A* (( *B*)*C*) rather
than, say, as (*A* *B*)*C* or as *A* ( (*B**C*)).

**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

· **Lr**_{e}* ^{G}*=

· **Wn**_{e}^{G}^{ }**á**G**ñ**** =** **Wn**_{e}^{A}**áΨ,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

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 **Un*** ^{G}*=

· **Lr**_{e}* ^{G}*={

· **Wn**_{e}^{G}^{ }**á**G**ñ**** =** ** **iff **Wn**_{e}^{A}**á**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 **(“

*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*_{0
}and_{ }*A*_{1 }are games_{ }with
a common universe *U*.

a)
*A*_{0 }_{ }*A*_{1}** **is defined as the
game *G* with **Un*** ^{G}*=

· **Lr**_{e}* ^{G}*={

· **Wn**_{e}^{G}**á** **ñ** =* *; **Wn**_{e}^{G}**á**** i**,G

b)
*A*_{0 }_{ }*A*_{1}** **is defined as the
game *G* with **Un*** ^{G}*=

·
**Lr*** ^{G}*={

· **Wn**^{G}**á** **ñ** = ; **Wn**^{G}**á**** i**,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**
(“

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 **Un*** ^{G}*=

· **Lr**_{e}* ^{G}*={

· **Wn**_{e}^{G}**á** **ñ** =* *; **Wn**_{e}^{G}**á**** c**,G

b)
*xA*(*x*) ** **is defined as the game *G* with **Un*** ^{G}*=

· **Lr**_{e}* ^{G}*={

· **Wn**_{e}^{G}**á** **ñ** =* *; **Wn**_{e}^{G}**á**** 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 *x**yA*(*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 *x**yA*(*y*=*x*+1), and the unary “generalized
successor” game of Figure 2.3.5 as *x**yA*(*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,** ***x**y*(*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
*x**yA*(*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 *x**y*(*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 *x**y*(*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?):

*x**y*(*Halts*(*x,y*) *Halts*(*x,y*)) *x**y*(*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** (“

**Definition
3.4.3** *A**B *=_{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 **(“

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 *A**B* is generally easier (at
least, not harder) to win than *A**B*,* *the latter is easier to win than *A**B*, and the latter in turn is
easier to win than *A**B*.

Technically, a move**α**in the left (resp. right) -conjunct or -disjunct is made by
prefixing **α**with ‘0.’. For instance, in
(the initial position of) (*A**B*)(*C**D*), 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 (*A**B*)*C*. The player
, too, has initial legal moves in (*A**B*)(*C**D*), 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. }**=

**Definition
3.5.2 **Assume** ***A*_{0
}and_{ }*A*_{1 }are games_{ }with
a common universe *U*.

a) *A*_{0}*A*_{1}** **is defined as the game *G* with **Un*** ^{G}*=

· F**Î**** Lr**_{e}* ^{G}* iff every move of F has
the prefix ‘0.’ or ‘1.’ and, for
both

· **Wn**_{e}^{G}**á**G**ñ** =* * iff, for
both *i***Î**{0,1}, **Wn**_{e}^{A}^{i}**á**G^{i}^{.}**ñ**=.

b) *A*_{0}*A*_{1}** **is defined as the game *G *with **Un*** ^{G}*=

· F**Î**** Lr**_{e}* ^{G}* iff every move of F has
the prefix ‘0.’ or ‘1.’ and, for
both

· **Wn**_{e}^{G}**á**G**ñ**=* *iff, for both *i***Î**{0,1}, **Wn**_{e}^{A}^{i}**á**G^{i}^{.}**ñ**=.

When *A* and *B* are
(constant) finite games, the depth of *A**B* or *A**B* 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* = *x**y*(*y*≠*x*^{2}) *x**y*(*y*=*x*^{2})
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:

*x**y*(*y*≠*x*^{2}) *x**y*(*y*=*x*^{2}) i.e. *A*

*x**y*(*y*≠*x*^{2}) *y*(*y*=7^{2}) i.e.
**á**1.7**ñ***A*

*y*(*y*≠7^{2}) *y*(*y*=7^{2})
i.e. **á**1.7,0.7**ñ***A*

49≠7^{2} *y*(*y*=7^{2})
i.e. **á**1.7,0.7,0.49**ñ***A*

49≠7^{2} 49=7^{2}
i.e. **á**1.7,0.7,0.49,1.49**ñ***A*

The run hits the true proposition 49≠7^{2} 49=7^{2},
and hence is won by the machine.

As we may guess, the ** parallel
universal quantification **(“

**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 **Un*** ^{G}*=

· **Φ****Î**** Lr**_{e}* ^{G}* iff every move of

· **Wn**_{e}^{G}**á**G**ñ** =* * iff, for
all *c*Î*Constants*, **Wn**_{e}^{A}**á**G^{c}^{.}**ñ**=.

b)
*xA*(*x*)** **is defined as the game *G* with **Un*** ^{G}*=

· **Φ****Î**** Lr**_{e}* ^{G}* iff every move of

· **Wn**_{e}^{G}**á**G**ñ**=* *iff, for all *c*Î*Constants*, **Wn**_{e}^{A}**á**G^{c}^{.}**ñ**=.

The remaining parallel operators are ** parallel
recurrence** (“

**Definition 3.5.6 **Assume *A* is
a game.

a) *A*** **is defined as the game *G* with **Un*** ^{G}*=

·
**Φ****Î**** Lr**_{e}* ^{G}* iff every move of

·
**Wn**_{e}^{G}**á**G**ñ** =* * iff, for
all *c*Î*Constants*, **Wn**_{e}^{A}**á**G^{c}^{.}**ñ**=.

b) *A*** **is defined as the game *G* with **Un*** ^{G}*=

· **Φ****Î**** Lr**_{e}* ^{G}* iff every move of

· **Wn**_{e}^{G}**á**G**ñ** =* ** *iff, for all *c*Î*Constants*, **Wn**_{e}^{A}**á**G^{c}^{.}**ñ**=.

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, *A**B *can be defined as* ** *