Game semantics

linear logic?*

* This material is based upon work supported by the National Science Foundation under Grant No. 0208816. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

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. The recently initiated line called **computability
logic** changes the approach and views games as foundational entities
in their own right. This approach is in the taste of those who believe
that syntax (axiomatizations or other deductive constructions) should serve
a meaningful and motivated semantics rather than vice versa.

The (new) concept of games that computability logic is based on appears to be an adequate
formal counterpart of our broadest intuition of ** interactive computational
tasks** --- tasks performed by a machine for a user/environment. What
is a task for a machine is a resource for the environment and vice versa,
so computability-logic 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 existence of a machine that always (under every particular
interpretation of atoms and against any possible behavior by the environment)
successfully accomplishes/provides/wins the task/resource/game represented
by the formula. With this semantics, *computability logic is a formal theory of
computability in the same sense as classical logic is a formal theory of
truth*. Furthermore, the classical concept of truth turns out to be
nothing but computability restricted to a special, so
called elementary sort of games, which translates into classical logic's
being nothing but a special --- elementary --- fragment of computability logic.

Please visit the Computability Logic Homepage to find out more about computability logic and related literature.

The set of valid formulas in a certain fragment of the (very expressive) language of computability logic forms a logic that is similar to but by no means the same as linear logic. The two logics typically agree on short and simple formulas: say, both of them reject A AA and accept A AA, with , and understood as what is respectively called linear implication, multiplicative conjunction and additive conjunction in linear logic, and reduction, parallel conjunction and choice conjunction in computability logic. On the other hand, computability logic disagrees with linear logic on longer formulas. E.g., computability logic validates the following two principles rejected even by affine logic (linear logic with the weakening rule):

(AB) (CD) (AC) (BD) (Blass's principle);

(A(CD)) (B(CD)) (C(AB)) (D(AB)) (AB) (CD),

with , , as before, and understood as what is called multiplicative disjunction in linear logic and parallel disjunction in computability logic.

Neither
the similarities nor the discrepancies are a surprise. The philosophies
of computability logic and linear logic overlap in their striving to develop a logic of resources.
But the ways this philosophy is materialized are radically opposite. Computability logic
starts with a mathematically strict and intuitively convincing semantics,
and only after that, as a natural second step, asks the question about
what the corresponding logic and its axiomatizations (syntax) are. It would
probably be accurate to say that linear logic,
on the other hand, started directly from the second step. As a logic of resources (rather than that of phases or coherence spaces), it was introduced
syntactically rather than semantically, essentially by taking classical
sequent calculus and throwing out the rules that seemed to be unacceptable
from the intuitive, naive resource point of view, so that in the absence
of a clear concept of truth or validity, the question about whether the
resulting system was sound/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. Apparently
the above formulas separating computability logic from linear logic should be considered examples
of such ¡°victims¡±. Of course, many attempts have been made to retroactively
find a missing semantical (mostly game-semantical) justification 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 right,
and how adequately it captures 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 Godel's completeness theorem. And this is exactly the scheme
that computability logic, too, follows.

Most relevant references:

- A.Blass.
*A game semantics for linear logic*.**Annals of Pure and Applied Logic**56 (1992), pp.183-220 - G.Japaridze.
*Introduction to cirquent calculus and abstract resource semantics*.**Journal of Logic and Computation**16 (2006), No.4 , pp. 489-532. - G.Japaridze.
*Cirquent calculus deepened*.**Journal of Logic and Computation**18 (2008), No.6, pp. 983-1028. - G.Japaridze.
*In the beginning was game semantics*. In:**Games: Unifying Logic, Language and Philosophy**. O.Majer, A.-V.Pietarinen and T.Tulenheimo, eds. Springer 2009, pp. 249-350.

(free-access online preprints of the above are also available on the Computability Logic Homepage)

Other game semantics links: