Arithmetics based on computability logic

##plugins.themes.bootstrap3.article.main##

Giorgi Japaridze

Abstract

This paper is a brief survey of number theories based on em computability logic (CoL) a game-semantically conceived logic of computational tasks of resources. Such theories, termed em clarithmetics, are conservative extensions of first-order Peano arithmetic. The first section of the paper lays out the conceptual basis of CoL and describes the relevant fragment of its formal language, with so called parallel connectives, choice connectives and quantifiers, and blind quantifiers. Both syntactically and semantically, this is a conservative generalization of the language of classical logic. Clarithmetics, based on the corresponding fragment of CoL in the same sense as Peano arithmetic is based on classical logic, are discussed in the second section. The axioms and inference rules of the system of clarithmetic named ${\bf CLA11}$ are presented, and the main results on this system are stated: constructive soundness, extensional completeness, and intensional completeness. In the final section two potential applications of clarithmetics are addressed: clarithmetics as declarative programming languages in an extreme sense, and as tools for separating computational complexity classes. When clarithmetics or similar CoL-based theories are viewed as programming languages, programming reduces to proof-search, as programs can be mechanically extracted from proofs; such programs also serves as their own formal verifications, thus fully neutralizing the notorious (and generally undecidable) program verification problem. The second application reduces the problem of separating various computational complexity classes to separating the corresponding versions of clarithmetic, the potential benefits of which stem from the belief that separating theories should generally be easier than separating complexity classes directly.

##plugins.generic.usageStats.downloads##

##plugins.generic.usageStats.noStats##

##plugins.themes.bootstrap3.article.details##

Section
Non-classical logics

References

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”, Information 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 2015 – Japaridze, G. “On the system CL12 of computability logic”, Logical Methods is Computer Science, 2015, Vol. 11, No. 3, Paper 1, pp. 1–71.
Japaridze 2016a – Japaridze, G. “Build your own clarithmetic I: Setup and completeness”, Logical Methods is Computer Science, 2016, Vol. 12, No. 3, Paper 8, pp. 1–59.
Japaridze 2016b – Japaridze, G. “Build your own clarithmetic II: Setup and completeness”, Logical Methods is Computer Science, 2016, Vol. 12, No. 3, Paper 12, pp. 1–62.
Japaridze 2016c – Japaridze, G. “Introduction to clarithmetic II”, Information and Computation, 2016, Vol. 247, pp. 290–312.