Computability logic

Introduced by Giorgi Japaridze in 2003, computability logic is a formal theory of computability in the same sense as classical logic is a formal theory of truth. That is, while the central semantical concept in classical logic is (Tarskian) truth, computability logic is based on a concept of computability. While the formulas of classical logic represent propositions or predicates, in computability logic they represent computational problems or, equivalently, computational resources. And, while validity in classical logic means being "always true", in computability logic it means being "always computable".

Computational problems/resources are understood in their most general - interactive sense. They are formalized as games played by a machine against the environment, with computability meaning existence of a machine that wins the game against any possible behavior by the environment. Defining, in precise terms, what such a game-playing machine means, computability logic provides a generalization of the Church-Turing thesis to the interactive level.

Computability logic appears to be the most serious and promising attempt to lay foundations for a comprehensive and systematic theory interactive computation.

References: G.Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1-99.

Main web source on the subject: Computability Logic Homepage