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: