Propositional Computability Logic II

TL;DR

This paper extends propositional computability logic from a minimal fragment to a more expressive system, CL2, incorporating two types of atoms to represent a broader class of computational problems, and proves its soundness and completeness.

Contribution

It introduces CL2, an extended propositional system with two atom types, and establishes its soundness and completeness, advancing the formal theory of computational tasks.

Findings

Proves soundness and completeness of CL2

Extends CL1 with elementary and general atoms

Demonstrates conservative extension of CL1

Abstract

Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as being a scheme of problems that always have algorithmic solutions. A comprehensive online source on the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html . The earlier article "Propositional computability logic I" proved soundness and completeness for the (in a sense) minimal nontrivial fragment CL1 of computability logic. The present paper extends that result to the significantly more expressive propositional system CL2. What makes CL2 more expressive than CL1 is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates), and general atoms, representing arbitrary computational problems. CL2 conservatively extends CL1, with the latter being nothing but the general-atom-free fragment of the former.