Soundness and completeness of the cirquent calculus system CL6 for computability logic

TL;DR

This paper proves that the cirquent calculus system CL6 is both sound and complete for computability logic, extending previous results from CL5 and integrating classical propositional logic.

Contribution

It extends the soundness and completeness results from CL5 to the more expressive CL6 system, which also encompasses classical propositional logic.

Findings

CL6 is sound for computability logic

CL6 is complete for computability logic

CL6 extends CL5 and classical propositional logic

Abstract

Computability logic is a formal theory of computability. The earlier article "Introduction to cirquent calculus and abstract resource semantics" by Japaridze proved soundness and completeness for the basic fragment CL5 of computability logic. The present article extends that result to the more expressive cirquent calculus system CL6, which is a conservative extension of both CL5 and classical propositional logic.