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 computable" problems. The present contribution gives a detailed exposition of a soundness and completeness proof for an axiomatization of one of the most basic fragments of computability logic. The logical vocabulary of this fragment contains operators for the so called parallel and choice operations, and its atoms represent elementary problems, i.e. predicates in the standard sense. This article is self-contained as it explains all relevant concepts. While not technically necessary, however, 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. Online introduction to the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html and http://www.csc.villanova.edu/~japaridz/CL/gsoll.html .

To appear in ACM Transactions on Computational Logic

References in corpus (2)

• Propositional computability logic I
• Computability Logic: a formal theory of interaction

Cited by in corpus (33)

• Sequential operators in computability logic
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Propositional computability logic I
• Computability Logic: a formal theory of interaction
• From truth to computability I
• The intuitionistic fragment of computability logic at the propositional level
• Propositional Computability Logic II
• Intuitionistic computability logic
• From truth to computability II
• Many concepts and two logics of algorithmic reduction
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Toggling operators in computability logic
• From formulas to cirquents in computability logic
• Introduction to clarithmetic II
• In the beginning was game semantics
• Towards applied theories based on computability logic
• A logical basis for constructive systems
• On the system CL12 of computability logic
• A new face of the branching recurrence of computability logic
• Introduction to clarithmetic I
• The taming of recurrences in computability logic through cirquent calculus, Part II
• Separating the basic logics of the basic recurrences
• The Computational Complexity of Propositional Cirquent Calculus
• Elementary-base cirquent calculus I: Parallel and choice connectives
• Build your own clarithmetic I: Setup and completeness
• Ptarithmetic
• Computability-logic web: an alternative to deep learning
• Towards Distributed Logic Programming based on Computability Logic
• Implementing Agent-Based Systems via Computability Logic CL2
• Implementing program extraction from CL1-proofs
• A PSPACE-Complete First Order Fragment of Computability Logic
• Soundness and completeness of the cirquent calculus system CL6 for computability logic
• Extending and Automating Basic Probability Theory with Propositional Computability Logic