Survey of Computability Logic

A Survey of

Computability Logic
გამოთვლადობის ლოგიკა
Логика вычислимости
可计算性逻辑
(CoL)

Computability is one of the most interesting and fundamental concepts in mathematics and computer science, and it is natural to ask what logic it induces. This is where Computability Logic (CoL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, CoL is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme “from truth to computability”.

Under the approach of CoL, logical operators stand for operations on computational problems, formulas represent such problems, and their “truth” is seen as algorithmic solvability. In turn, computational problems --- understood in their most general, interactive sense --- are defined as games played by a machine against its environment, with “algorithmic solvability” meaning existence of a machine which wins the game against any possible behavior of the environment. With this semantics, CoL provides a systematic answer to the question “what can be computed?”, just like classical logic is a systematic tool for telling what is true. Furthermore, as it happens, in positive cases “what can be computed” always allows itself to be replaced by “how can be computed”, which makes CoL of potential interest in not only theoretical computer science, but many applied areas as well, including constructive applied theories, interactive knowledgebase systems, resource oriented systems for planning and action, or declarative programming languages.

Currently CoL is still at an early stage of development, with open problems prevailing over answered questions. For this reason it offers plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science.

This article presents a survey of the subject: its philosophy and motivations, main concepts and most significant results obtained so far. No proofs of those results are included.

Contents

1 The philosophy of CoL

1.1 Syntax vs. semantics

1.2 Why game semantics?

1.3 CoL vs. classical logic

1.4 CoL vs. linear logic

1.5 CoL vs. intuitionistic logic

1.6 CoL vs. independence-friendly logic

1.7 The ‘from semantics to syntax’ paradigm

2 Games

2.1 The two players

2.2 Moves, runs and positions