* 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:
(free-access online preprints of the above are also available on the Computability Logic Homepage)
Other game semantics links: