Computability Logic: A Formal Theory of Interactive Computability

Title: Computability Logic: A Formal Theory of Interactive Computability

Research Question: How can computability logic, a new approach to understanding computational problems, help us better understand and formalize the concept of interactive computability?

Methodology: The authors propose a new approach called computability logic (CL), which views computational problems as games played by a machine against the environment. The machine's goal is to always win the game, and logical operators are seen as operations on computational problems. The validity of a logical formula is then defined as a scheme of "always computable" problems.

Results: The authors introduce the concept of interaction histories, where the machine and environment communicate with each other through observable actions. They also define games and runs, with "possible" interaction histories being legal runs and "successful" interaction histories being won runs. They show that traditional computational problems can be modeled as two-move-deep games, where the machine must win against any possible environment behavior.

Implications: The development of CL reveals that the traditional, non-interactive concept of computability may be too narrow and artificially delimited. It suggests that a more general, interactive approach to computability is necessary to capture the full range of our computational problem-solving intuition. The authors believe that CL can provide a solid foundation for further research in this area and potentially lead to new insights and developments in computer science.

Link to Article: https://arxiv.org/abs/0404024v3 Authors: arXiv ID: 0404024v3