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.
 

• Computability Logic Homepage
• Author's homepage (Giorgi Japaridze)

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:

• Linear Logic papers of Andreas R. Blass