In the beginning was game semantics. (English) Zbl 1171.03015

Japaridze, Giorgi

Majer, Ondrej (ed.) et al., Games: Unifying logic, language, and philosophy. Berlin: Springer (ISBN 978-1-4020-9373-9/hbk; 978-1-4020-9374-6/e-book). Logic, Epistemology, and the Unity of Science 15, 249-350 (2009).

The article is an overview of works about computability logic (CL) as a formal-logic axiomatic system formalizing the process of computation considered as interactive game between a machine and its environment. Semantics of the formalism are game semantics. For CL, ‘game’ is a foundational mathematical concept on which a powerful enough logic (=semantics) is based. As the author affirms, CL sees logic as a “real-life navigational tool” and games offer comprehensive, coherent, natural, adequate and convenient mathematical models for the essence of all “navigational” activities of agents: their interactions with the surrounding world, where an agent and its environment translate into game-theoretical terms as two players; their actions as moves; situations arising in the course of interaction as positions; and success or failure as wins or losses. The interaction strategies (the agents) of the party are limited to algorithmic ones, allowing to call that player a machine. Algorithmic activity is a computation, games 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.
The author supposes that CL falls outside the limits of possibilities of Turing machines.
The philosophy of CL relies on two beliefs which can be considered as interactive version of the Church-Turing thesis: 1) the concept of static games is an adequate formal counterpart of the intuition of interactive computational problems; 2) the concept of winnability is an adequate formal counterpart of the intuition of algorithmic solvability of such problems.
The soundness of affine logic with respect to the semantics of CL is proved.
For the entire collection see [Zbl 1154.03004].

Reviewer: Alex Nabebin (Moskva)

MSC:

03B60	Other nonclassical logic
03B70	Logic in computer science
03F52	Proof-theoretic aspects of linear logic and other substructural logics
68Q05	Models of computation (Turing machines, etc.) (MSC2010)
91A80	Applications of game theory

Keywords:

computability logic; interactive computation; game semantics; winnability; linear logic; constructive logics; affine logic; survey paper