Computability 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.
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. Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.
...
Wikipedia