Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with (...) respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logic-based Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings—an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems. (shrink)

This work is an attempt to lay foundations for a theory of interactive computation and bring logic and theory of computing closer together. It semantically introduces a logic of computability and sets a program for studying various aspects of that logic. The intuitive notion of computational problems is formalized as a certain new, procedural-rule-free sort of games between the machine and the environment, and computability is understood as existence of an interactive Turing machine that wins the game against any possible (...) environment. The formalism used as a specification language for computational problems, called the universal language, is a non-disjoint union of the formalisms of classical, intuitionistic and linear logics, with logical operators interpreted as certain—most basic and natural—operations on problems. Validity of a formula is understood as being “always computable”, and the set of all valid formulas is called the universal logic. The name “universal” is related to the potential of this logic to integrate, on the basis of one semantics, classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. In particular, the classical notion of truth turns out to be nothing but computability restricted to the formulas of the classical fragment of the universal language, which makes classical logic a natural syntactic fragment of the universal logic. The same appears to be the case for intuitionistic and linear logics . Unlike classical logic, these two do not have a good concept of truth, and the notion of computability restricted to the corresponding two fragments of the universal language, based on the intuitions that it formalizes, can well qualify as “intuitionistic truth” and “linear-logic truth”. The paper also provides illustrations of potential applications of the universal logic in knowledgebase, resourcebase and planning systems, as well as constructive applied theories. The author has tried to make this article easy to read. It is fully self-contained and can be understood without any specialized knowledge of any particular subfield of logic or computer science. (shrink)

Within the program of finding axiomatizations for various parts of computability logic, it was proven earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting’s intuitionistic calculus. That sort of reduction permits unlimited reusage of the computational resource represented by the antecedent. An at least equally basic and natural sort of algorithmic reduction, however, is the one that does not allow such reusage. The present article shows that turning the logic of the first sort of (...) reduction into the logic of the second sort of reduction takes nothing more than just deleting the contraction rule from its Gentzen-style axiomatization. The first sort of interactive reduction is also shown to come in three natural versions. While those three versions are very different from each other, their logical behaviors turn out to be indistinguishable, with that common behavior being precisely captured by implicative intuitionistic logic. Among the other contributions of the present article is an informal introduction of a series of new — finite and bounded — versions of recurrence operations and the associated reduction operations. (shrink)