Computability logic: Giving Caesar what belongs to Caesar


Giorgi Japaridze


The present article is a brief informal survey o$\textit {computability logic}$ (CoL). This relatively young and still evolving nonclassical logic can be characterized as a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader sense, being conceived semantically rather than proof-theoretically, CoL is not just a particular theory but an ambitious and challenging long-term project for redeveloping logic.

In 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 a problem-solving tool.

CoL is a conservative extension of classical first order logic but is otherwise much more expressive than the latter, opening a wide range of new application areas. It relates to intuitionistic and linear logics in a similar fashion, which allows us to say that CoL reconciles and unifies the three traditions of logical thought (and beyond) on the basis of its natural and "universal" game semantics.




Non-classical logics


Blass, 1992 – Blass, A. “A game semantics for linear logic”, Annals of Pure and Applied Logic, 1992, Vol. 56, pp. 183–220.
Hintikka, 1973 – Hintikka, J. Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic. Clarendon Press, 1973.
Japaridze, 2003 – Japaridze, G. “Introduction to computability logic”, Annals of Pure and Applied Logic, 2003, Vol. 123, pp. 1–99.
Japaridze, 2007a – Japaridze, G. “Introduction to computability logic”, Acta Cybernetica, 2007, Vol. 18, No. 1, pp. 77–113.
Japaridze, 2007b – Japaridze, G. “The intuitionistic fragment of computability logic at the propositional level”, Annals of Pure and Applied Logic, 2007, Vol. 143, No. 1, pp. 187–227.
Japaridze, 2009 – Japaridze, G. “In the beginning was game semantics”, in: Games: Unifying Logic, Language, and Philosophy, eds. by O. Majer, A.-V. Pietarinen and T. Tulenheimo. Springer, 2009, pp. 249–350.
Japaridze, 2010 – Japaridze, G. “Towards applied theories based on computability logic”, Journal of Symbolic Logic, 2010, Vol. 75, pp. 565–601.
Japaridze, 2011 – Japaridze, G. “Introduction to clarithmetic I”, nformation and Computation, 2011, Vol. 209, pp. 1312–1354.
Japaridze, 2014 – Japaridze, G. “Introduction to clarithmetic III”, Annals of Pure and Applied Logic, 2014, Vol. 165, pp. 241–252.
Japaridze, 2016a – Japaridze, G. “Introduction to clarithmetic II”, Information and Computation, 2016, Vol. 247, pp. 290–312.
Japaridze, 2016b – Japaridze, G. “Build your own clarithmetic I: Setup and completeness”, Logical Methods in Computer Science, 2016, Vol. 12, Issue 3, Paper 8, pp. 1–59.
Japaridze, 2016c – Japaridze, G. “Build your own clarithmetic II: Soundness”, Logical Methods in Computer Science, 2016, Vol. 12, Issue 3, Paper 12, pp. 1–62.
Japaridze, 2019 – Japaridze, G. “Computability Logic Homepage”, An Online Survey of Computability Logic. 2019. [$\sim$japaridz/CL/, accessed on 21.02.2019]
Kolmogorov, 1932 – Kolmogorov, A. N. “Zur Deutung der intuitionistischen Logik”, Mathematische Zeitschrift, 1932, Vol. 35, pp. 58–65.
Lorenzen, 1961 – Lorenzen, P. “Ein dialogisches Konstruktivit¨atskriterium”, in: Infinitistic Methods. PWN, Proc. Symp. Foundations of Mathematics., Warsaw, 1961, pp. 193–200.
Mezhirov, Vereshchagin, 2010 – Mezhirov, I., Vereshchagin, N. “On abstract resource semantics and computability logic”, Journal of Computer and Systems Sciences, 2010, Vol. 76, pp. 356–372.
Turing, 1936 – Turing, A. “On Computable numbers with an application to the entsheidungsproblem”, Proceedings of the London Mathematical Society, 1936, Vol. 2:42, pp. 230–265.