Computability logic - AbsoluteAstronomy.com

Giorgi Japaridze

Giorgi Japaridze is a logician, at Villanova University in Villanova, Pennsylvania. In the past his contributions were primarily into the areas of provability logic and interpretability logic...

in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability

Recursion theory

Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...

, as opposed to classical logic

Classical logic

Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...

which is a formal theory of truth. In this approach logical formulas represent computational problems (or, equivalently, computational resources), and their validity means being "always computable".

Computational problems and resources are understood 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, computability logic 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 computability logic. Being a conservative extension

Conservative extension

In mathematical logic, a logical theory T_2 is a conservative extension of a theory T_1 if the language of T_2 extends the language of T_1; every theorem of T_1 is a theorem of T_2; and any theorem of T_2 which is in the language of T_1 is already a theorem of T_1.More generally, if Γ is a set of...

of the former, computability logic is, at the same time, by an order of magnitude more expressive, constructive and computationally meaningful. Providing a systematic answer to the fundamental question "what (and how) can be computed?", it has a wide range of potential application areas. Those include constructive applied theories, knowledge base systems, systems for planning and action.

Besides classical logic, linear logic

Linear logic

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...

(understood in a relaxed sense) and intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

also turn out to be natural fragments of computability logic. Hence meaningful concepts of "intuitionistic truth" and "linear-logic truth" can be derived from the semantics of computability logic.

Being semantically constructed, as yet computability logic does not have a fully developed proof theory. Finding deductive system

Deductive system

A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....

s for various fragments of it and exploring their syntactic properties is an area of ongoing research.

External links

See also