Propositional computability logic I

ABSTRACT

In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity of a logical formula as being a scheme of “always computabl ” problems. Computability logic has been introduced semantically, and now among its main technical goals is to axiomatize the set of valid formulas or various natural fragments of that set. The present contribution signifies a first step towards this goal. It gives a detailed exposition of a soundness and completeness proof for the rather new type of a deductive propositional system CL1, the logical vocabulary of which contains operators for the so called parallel and choice operations, and the atoms of which represent elementary problems, that is, predicates in the standard sense.This article is self-contained as it explains all relevant concepts. While not technically necessary, familiarity with the foundational paper “Introduction to Computability Logi ” [Annals of Pure and Applied Logic 123 (2003), pp.1-99] would greatly help the reader in understanding the philosophy, underlying motivations, potential and utility of computability logic---the context that determines the value of the present results.

REFERENCES

• 1: Samson Abramsky , Radha Jagadeesan, Games and full completeness for multiplicative linear logic, Journal of Symbolic Logic, v.59 n.2, p.543-574, June 1994 [doi>10.2307/2275407]
• 2: van Benthem, J. 2001. Logic in games. Tech. rep., University of Amsterdam. ILLC preprint.
• 3: Blass, A. 1992. A game semantics for linear logic. Ann. Pure Appl. Logic 56, 183--220.
• 4: Dina Q. Goldin, Persistent Turing Machines as a Model of Interactive Computation, Proceedings of the First International Symposium on Foundations of Information and Knowledge Systems, p.116-135, February 14-17, 2000
• 5: Japaridze, G. 1997. A constructive game semantics for the language of linear logic. Ann. Pure Appl. Logic 85, 87--156.
• 6: Japaridze, G. 2002. The logic of tasks. Ann. Pure Appl. Logic 117, 263--295.
• 7: Japaridze, G. 2003. Introduction to computability logic. Ann. Pure Appl. Logic 123, 1--99.
• 8: Japaridze, G. 2004. Computability logic: A formal theory of interaction. Tech. Rep. arXiv:cs.LO/0404024, Villanova University. http://arxiv.org/abs/cs.LO/0404024.
• 9: Lorenzen, P. 1961. Ein dialogishes Konstruktivitätskriterium. In Proceedings of the Symposium on Foundations of Mathematics. PWN, (Warsaw) 193--200.
• 10: Robin Milner, Elements of interaction: Turing award lecture, Communications of the ACM, v.36 n.1, p.78-89, Jan. 1993 [doi>10.1145/151233.151240]
• 11: Turing, A. 1936. On computable numbers with an application to the Entscheidungsproblem. In Proceedings of the London Mathematical Society 2:42, 230--265.
• 12: Peter Wegner, Interactive foundations of computing, Theoretical Computer Science, v.192 n.2, p.315-351, Feb. 20, 1998 [doi>10.1016/S0304-3975(97)00154-0 ]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation

General Terms:
Theory

Keywords:
Computability logic, computational resources, game semantics, interactive algorithms, linear logic