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

TL;DR

This paper introduces a cirquent calculus system for computability logic, establishing its soundness and setting the stage for a completeness proof, thereby advancing the formal understanding of logical recurrences.

Contribution

It constructs a new cirquent calculus system for computability logic and proves its soundness, contributing a foundational framework for handling recurrences.

Findings

System is sound with respect to computability logic semantics

Defines a logical vocabulary including negation, conjunction, disjunction, and recurrences

Prepares groundwork for a completeness proof in Part II

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 present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.