Jump to content

Computability logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Anaszt5 (talk | contribs) at 01:58, 8 October 2016 (Updated content; tagged with "mathlogic-stub".). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
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. While in classical logic formulas 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.[1][2] Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.

The traditional proof systems such as natural deduction or sequent calculus turn out to be inapplicable for axiomatizing CoL or nontrivial fragments of it. This has necessitated developing alternative, more general and flexible methods of proof, such as cirquent calculus.

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 as computationally and complexity-theoretically meaningful alternatives to the classical-logic-based Peano arithmetic and its variations such as systems of bounded arithmetic.

The program was officially introduced and named "Computability logic" (not to be confused with the generic term “computational logic”) by Giorgi Japaridze in 2003.[3] Despite steady progress since then, according to Japaridze,[4] CoL still remains at an early stage of development with many open problems.

Literature

See also

References

  1. ^ 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.
  2. ^ G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
  3. ^ G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
  4. ^ Computability Logic Homepage
Stub icon

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Computability_logic&oldid=743137253"