The taming of recurrences in computability logic through cirquent calculus, Part II

TL;DR

This paper develops a cirquent calculus system for computability logic, establishing its soundness and completeness, thereby advancing the formal framework for reasoning about computational problems with complex recurrence operators.

Contribution

It introduces a new cirquent calculus system for computability logic and proves its soundness and completeness, enhancing the formal tools for computational reasoning.

Findings

The system is sound with respect to computability logic semantics.

The system is complete, capturing all valid formulas in the logic.

It extends previous work with a focus on recurrence operators.

Abstract

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. The article is published in two parts, with (the previous) Part I containing preliminaries and a soundness proof, and (the present) Part II containing a completeness proof.