**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

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.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.3
Constant games

2.4
Not-necessarily-constant
games

2.5
Static games

3
The CoL zoo of game
operations

3.1 Preview

3.2
Prefixation

3.3 Negation

3.6
Reduction

3.7
Blind operations

3.10
Toggling operations

3.11
Cirquents

5
The
language
of CoL and its semantics

5.1
Formulas

5.2
Interpretations

5.3
Validity

6.1
Outline

6.2
The Gentzen-style
system **CL7**

6.3
The Gentzen-style
system **Int ^{+}**

6.4
The cirquent
calculus system **CL15**

6.5
The brute force
system **CL13**

6.6
The brute force
system **CL4**

6.7
The brute force
system **CL12**

7
Clarithmetic (CoL-based
arithmetic)

7.1
Introduction

7.2
Clarithmetic versus
bounded arithmetic

7.3
Motivations

7.4
Common preliminaries
for all our theories of
clarithmetic

7.6
Clarithmetics for
provable computability

8
CoL-based knowledgebase
and resourcebase systems

9.1
Selected papers on
CoL by Japaridze

9.2
Selected papers on
CoL by other authors

9.3
PhD theses, MS
theses and externally funded
projects on CoL