Propositional computability logic I

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 computable" 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 Logic" [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.