Editing Computability logic (section)

{{Short description|A framework for studying interactive computational tasks through logic.}}
{{distinguish|Computational logic}}
{{One source|text=All references in this article are exclusively by a single author, G. Japaridze.|date=May 2020}}
'''Computability logic''' ('''CoL''') is a research program and mathematical framework for redeveloping [[mathematical logic|logic]] as a systematic formal theory of [[computability]], as opposed to [[classical logic]], which is a formal theory of [[truth]]. It was introduced and so named by [[Giorgi Japaridze]] in 2003.<ref> G. Japaridze, ''Introduction to computability logic''. [[Annals of Pure and Applied Logic]] 123 (2003), pages 1–99. {{doi|10.1016/S0168-0072(03)00023-X}}</ref> 

In classical logic, [[formula (logic)|formula]]s represent true/false [[statement (logic)|statement]]s. In CoL, formulas represent [[computational problem]]s. In classical logic, the validity of an argument depends only on its form, not on its meaning. In CoL, validity means being always computable. More generally, classical logic tells us when the truth of a given statement always follows from the truth of a given set of other statements. Similarly, CoL tells us when the computability of a given problem  ''A'' always follows from the computability of other given problems ''B<sub>1</sub>,...,B<sub>n</sub>''. Moreover, it provides a uniform way to actually construct a solution ([[algorithm]]) for such an ''A'' from any known solutions of ''B<sub>1</sub>,...,B<sub>n</sub>''.

CoL formulates computational problems in their most general—[[Interactive computation|interactive]]—sense. CoL defines a ''computational problem'' as a game played by a machine against its environment. Such a problem is ''computable'' if there is a machine that wins the game against every possible behavior of the environment. Such a game-playing machine generalizes the [[Church–Turing thesis]] to the interactive level. The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of CoL. Thus CoL is a [[conservative extension]] of classical logic. Computability logic is more [[Expressive power (computer science)|expressive]], constructive and computationally meaningful than classical logic. Besides classical logic, [[independence-friendly logic|independence-friendly (IF) logic]]  and certain proper extensions of [[linear logic]] and [[intuitionistic logic]] also turn out to be natural fragments of CoL.<ref>G. Japaridze, ''In the beginning was game semantics?''.   Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp.&nbsp;249–350. {{doi|10.1007/978-1-4020-9374-6_11}} [https://arxiv.org/abs/cs/0507045 Prepublication]</ref><ref>G. Japaridze, ''The intuitionistic fragment of computability logic at the propositional level''. Annals of Pure and Applied Logic 147 (2007), pages 187–227. {{doi|10.1016/j.apal.2007.05.001}}</ref> Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.

CoL systematically answers the fundamental question of what can be computed and how; thus CoL has many applications, such as constructive applied theories, [[knowledge base]] systems, systems for planning and action. Out of these, only applications in constructive applied theories have been extensively explored so far: a series of CoL-based number theories, termed "clarithmetics", have been constructed<ref>G. Japaridze, ''Introduction to clarithmetic I''. [[Information and Computation]] 209 (2011),  pp.&nbsp;1312–1354. {{doi|10.1016/j.ic.2011.07.002}} [https://arxiv.org/abs/1003.4719 Prepublication]</ref><ref>G. Japaridze, ''[https://lmcs.episciences.org/2020/pdf Build your own clarithmetic I: Setup and completeness]''. [[Logical Methods in Computer Science]] 12 (2016), Issue 3, paper 8, pp.&nbsp;1–59.</ref> as computationally and [[Computational complexity theory|complexity-theoretically]] meaningful alternatives to the classical-logic-based [[Peano_axioms#Peano_arithmetic_as_first-order_theory|first-order Peano arithmetic]] and its variations such as systems of [[bounded arithmetic]].

Traditional proof systems such as [[natural deduction]] and [[sequent calculus]] are insufficient for axiomatizing nontrivial fragments of CoL. This has necessitated developing alternative, more general and flexible methods of proof, such as [[cirquent calculus]].<ref>G. Japaridze, ''Introduction to cirquent calculus and abstract resource semantics''. [[Journal of Logic and Computation]] 16 (2006),  pages 489–532. {{doi|10.1093/logcom/exl005}} [https://arxiv.org/abs/math/0506553 Prepublication]</ref><ref>G. Japaridze, ''The taming of recurrences in computability logic through cirquent calculus, Part I''. [[Archive for Mathematical Logic]] 52 (2013), pp.&nbsp;173–212. {{doi|10.1007/s00153-012-0313-8}} [https://arxiv.org/abs/1105.3853 Prepublication]</ref>