* 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.
What is computability
logic? Computability is certainly one of the most interesting and fundamental
concepts in mathematics and computer science, and it would be more than
natural to ask what logic it induces. Let us face
it: this question has not only never been answered, but never even been
asked
within a reasonably coherent and comprehensive formal framework.
This is where Computability Logic 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, computability logic is not just a particular theory but an
ambitious and challenging program for redeveloping logic following the scheme
"from truth to computability". It was introduced in 2003 and, at present, still
remains in its infancy stage, with open problems prevailing over answered
questions. It is largely a virgin soil offering plenty of research
opportunities, with good chances of interesting findings, for those with
interests in logic and its applications in computer science.
Computation and computational problems in computability logic are understood in their most
general, interactive sense, and are precisely seen as games played by a
machine (computer, agent, robot) against its environment (user, nature,
or the devil himself). Computability of such problems means existence of a
machine that always wins the game. Logical operators stand for operations on
computational problems, and validity of a logical formula means being a scheme
of "always computable" problems.
Remarkably, classical, intuitionistic and linear (in a broad sense)
logics turn out to be three natural fragments of computability logic.
This is no accident. The classical concept of truth is
nothing but a special case of computability -- computability restricted
to problems of zero interactivity degree. Correspondingly, classical
logic is nothing but a special fragment of computability logic. One of the main -- so far
rather abstract -- intuitions associated with intuitionistic logic is
that it must be a logic of problems (Kolmogorov 1932); this is exactly what
computability logic is, only in a much more expressive language than intuitionistic
logic. And one of the main -- again, so far rather abstract -- claims of linear
logic is that it is a logic of resources. Reversing of the roles of the machine
and its environment turns computational problems into computational resources,
which makes computability logic a logic of resources, only, again, in a more
expressive language than that of linear logic, and based on an intuitively
convincing and mathematically strict resource semantics rather than some naive
philosophy and unreliable syntactic arguments. For more about computability
logic vs. linear logic,
visit Game
Semantics or Linear Logic?.
Potential applications of
computability logic: The computability logic paradigm is not only about "what can be computed", but
equally about "how can be computed". This opens application
areas far beyond pure computation theory, such as:
Knowledgebase systems.
Computability logic is an appealing alternative to the traditional knowledge base,
knowledge representation and query logics. Its advantages include:
Computability logic is a logic of interaction, and this is what a good
knowledgebase logic needs to be. After all, most of the real knowledgebase and
information systems are interactive.
Computability logic is resource-conscious: the potential knowledge provided by a disposable pregnancy test device
is knowledge of only one (even though an arbitrary one) woman's
pregnancy status, but not two. Computability logic naturally captures
this sort of extremely relevant differences while
the traditional systems fail to account for them.
Computability logic naturally differentiates between truth and an agent's actual
ability to find/compute/tell what is true. To achieve similar effects,
traditional knowledgebase logics have to appeal to the controversial,
messy and troublemaking epistemic constructs.
Systems for planning and action.
Computability logic might be a reasonable alternative to the traditional AI
planning logics. Its advantages include:
Computability logic is a logic of interaction, and planning systems
should be well able to account for an agent's interaction with the
environment.
A good planning logic should be able to naturally account for the fact that
with one ballistic missile one can destroy only one (even though an arbitrary
one) target but not two. The resource-conscious computability logic fits the bill.
Computability logic is a logic of knowledge and informational resources, which
automatically takes care of the knowledge preconditions problem.
Computability-logic-based planning systems are immune to the notorious frame
problem.
Constructive applied theories.
Computability logic is a conservative extension of classical logic, which makes it
a reasonable alternative to the latter in its most traditional and unchallenged
application areas. In particular, it makes perfect sense to base
applied theories (such as, say, Peano arithmetic) on computability logic instead of
classical logic.
The advantages of doing so include that computability-logic-based applied theories,
compared with their classical-logic-based counterparts, are:
Expressive: the language of classical logic is only a modest fraction of
the language of computability logic.
Computationally meaningful: every theorem of a computability-logic-based
theory represents a computable problem rather than just a true
statement.
Constructive: any proof of a formula F in a computability-logic-based theory effectively
encodes a solution to the computational problem represented by F.
Selected papers on
computability logic:
The official journal versions of the following papers may be slightly different
from the corresponding online preprints. It is recommended that you try to use
the journal version first. Access to some journals may be restricted though, in
which case you may download the online preprint.
Recommendation: For the first
acquaintance with the subject, most recommended is reading the tutorial-style
Sections 1-10 of "In the beginning was game semantics".
[4]
G.Japaridze,
Introduction to cirquent calculus and abstract resource
semantics.Journal of Logic and Computation
16 (2006), No.4, pp. 489-532.
Official journal version
Online preprint Cirquent calculus is a new syntactic approach, which can be seen as a
refinement of sequent calculus. Unlike the latter, it is flexible enough to be
used as a deductive framework for computability logic.
¡¡
[5]
G.Japaridze,
Computability logic: a formal theory of interaction.
In: Interactive
Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds.
Springer 2006, pp. 183-223.
Official book
version
Online preprint Presents a relatively compact and nontechnical introduction to
computability logic and an
overview of the newest
results. Most recommended for those whose primary interests are in
computer science. Written
in a semitutorial style with non-expert audience in mind. ¡¡
[6]
G.Japaridze,
From truth to computability I.Theoretical Computer Science 357 (2006), pp. 100-135.
Official journal versionOnline preprint Proves soundness and completeness for the first-order fragment CL3
of computability logic, which is the predicate version of logic CL1
studied in [2].
¡¡
[7] G.Japaridze,
From truth to computability II.Theoretical Computer Science
379 (2007), pp. 20-52.
Official journal versionOnline preprint Extends the results of its predecessor in the same sense on
the first-order level as [3] extends [2] on the propositional level.
¡¡
[8] G.Japaridze,
Intuitionistic computability logic.Acta
Cybernetica18 (2007), No.1, pp.77-113.
Official journal versionOnline preprint Proves soundness for Heyting's intuitionistic predicate calculus
with respect to the computability-logic semantics. ¡¡
[9]
G.Japaridze,
The logic of interactive Turing reduction.Journal of Symbolic
Logic 72 (2007), No.1, pp. 243-276.
Official journal versionOnline preprint A proof of the completeness of the imlicative fragment of
intuitionistic logic with respect to the semantics of computability logic. ¡¡
[10]
G.Japaridze,
The intuitionistic fragment of computability logic at the
propositional level.Annals of Pure and
Applied Logic 147 (2007), No.3, pp.187-227. Official journal versionOnline preprint Proof of the (soundness and) completeness of the full propositional intuitionistic logic with respect to the semantics of computability logic.
¡¡
[11] G.Japaridze,
Cirquent calculus deepened.Journal of Logic and Computation
18 (2008), No.6, pp.983-1028. Official journal versionOnline preprint Elaborates a
deep version (as opposed to the shallow version of [4]) of cirquent calculus for
the (Ø,Ú,Ù)-fragment of computability logic and
classical propositional logic.
¡¡
[12] G.Japaridze, Sequential operators in computability logic.Information and Computation
206 (2008), No.12, pp. 1443-1475. Official journal versionOnline preprint
Introduces the new, sequential group (conjunction/disjunction, quantifiers and
recurrences) of game operations. Constructs sound and complete axiomatizations.
¡¡
[13] 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.
Official book versionOnline preprint A comprehensive overview of the philosophy, motivations and
techniques of computability logic. Supported by ample illustrations and examples.
Contains a proof of the soundness of affine logic, claimed but never
officially proven before.
¡¡
[14] G.Japaridze, Many concepts and two logics of algorithmic reduction.Studia Logica 91 (2009),
No.1, pp. 1-24.
Official journal versionOnline preprint The main result here is a proof of the fact that implicative binary tautologies and their instances are precisely captured by the implicative fragment of intuitionistic calculus without contraction. This is the logic of the basic (linear) sort of reduction.
¡¡
[15] G.Japaridze, Towards applied theories based on computability logic.Journal of Symbolic
Logic (under review). 30 pages. Official journal version
Online preprint Basing Peano
arithmetic on computability logic instead of classical logic. Built on the new sound and complete
deductive system CL12 for computability logic, which substantially strengthens the system
CL3 introduced in [6].
¡¡
[16] G.Japaridze, Ptarithmetic.Information and Computation
(under review). 100 pages. Official journal version
Online preprint Constructs a
computability-logic-based arithmetic that proves precisely the number-theoretic
problems that have polynomial time solutions. ¡¡
[17] G.Japaridze,
Toggling operators in computability logic.Theoretical Computer Science
(under review). 40 pages.
Official journal version
Online preprint Introduces the
new, toggling ("trial-and-error") group of game operations
(conjunction/disjunction, quantifiers and recurrences). Constructs a sound and complete axiomatization
for the fragment of computability logic which, along with negation, has all four
--- parallel, toggling, sequential and choice --- sorts of conjunctions and
disjunctions. ¡¡
[18] G.Japaridze,
From formulas to cirquents in computability logic.Annals of Pure and
Applied Logic (under review). 42 pages.
Official journal version
Online preprint Brings
cirquents into computability logic. Brings together computability logic and
independence-friendly logic.