(CoL)

Section 1

**The philosophy of CoL**

1.5
CoL vs.
intuitionistic logic

1.6
CoL vs.
independence-friendly logic

1.7 The ‘from
semantics
to syntax’ paradigm

** **

1.1 Syntax vs. semantics

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, game is 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 celebrated 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 see this, it is
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. Understanding those operations as logical operators, it then
looks
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.

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. (Those
who want to exclaim "But what about,
say, the phase or coherence space semantics?!" are kindly asked
to read the rest of this subsection as well as Subsection 1.7). In fact, the semantics of
CoL can be seen as such a justification, but 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,*accepted by CoL but rejected by affine logic.

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 introduced syntactically rather than semantically,
essentially by taking classical sequent calculus and deleting the rules
that
seemed unacceptable from a certain intuitive, naive and never
formalized "resource-semantical" point of
view. 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. The latter, just like linear logic, is sound with respect
to resource semantics, whatever such a semantics
means; it is sound with respect to any semantics for that matter.

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

In full
generality,
the “linear-logic fragment” of CoL is strictly between affine 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, negation, 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 just 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 and unlike linear or intuitionistic
logics, 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 is 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* (