Computability logic

Not to be confused with computational logic.

Computability logic (CoL) is a research program and mathematical framework for redeveloping 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.[1]

Comparing CoL with classical logic, while formulas in the latter represent true/false statements, in CoL they represent computational problems. In classical logic, validity of a formula is understood as being always true, i.e., true regardless of the interpretation of its non-logical primitives (atoms), based solely on form rather than meaning. Similarly, 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 B1,…,Bn. Moreover, it provides a uniform way to actually construct a solution (algorithm) for such an A from any known solutions of B1,…,Bn.

CoL understands computational problems in their most general - interactive sense. They are formalized as games played by a machine against its environment, and computability means existence of a machine that wins the game against any possible behavior by the environment. Defining what such game-playing machines mean, CoL provides a generalization of 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. Being a conservative extension of the former, computability logic is, at the same time, by an order of magnitude more expressive, constructive and computationally meaningful. Besides classical logic, independence-friendly (IF) logic and certain proper extensions of linear logic and intuitionistic logic also turn out to be natural fragments of CoL.[2][3] Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.

Providing a systematic answer to the fundamental question of what can be computed and how, CoL claims a wide range of potential application areas. Those include 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[4][5] as computationally and complexity-theoretically meaningful alternatives to the classical-logic-based Peano arithmetic and its variations such as systems of bounded arithmetic.

The traditional proof systems such as natural deduction or sequent calculus turn out to be insufficient for axiomatizing any more or less nontrivial fragments of CoL. This has necessitated developing alternative, more general and flexible methods of proof, such as cirquent calculus.[6][7]


Literature

External links

See also

References

  1. ↑ G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
  2. ↑ 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. 249–350. Prepublication
  3. ↑ G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
  4. ↑ G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354. Prepublication
  5. ↑ G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1-59.
  6. ↑ G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532. Prepublication
  7. ↑ G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173-212. Prepublication
This article is issued from Wikipedia - version of the 10/17/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.