A propositional cirquent calculus for computability logic

TL;DR

This paper introduces a new proof system called CL18 for propositional computability logic, capturing computational resources and tasks through cirquent calculus with sharing, and proves its soundness and completeness.

Contribution

It constructs an axiomatization of propositional computability logic using cirquent calculus, demonstrating its soundness and completeness relative to game-semantical semantics.

Findings

CL18 is sound for propositional computability logic.

CL18 is complete for propositional computability logic.

The system effectively models computational resources and tasks.

Abstract

Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18 of the basic propositional fragment of computability logic the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical result of the article is a proof of the soundness and completeness of CL18 with respect to the semantics of computability logic.