This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\neg}}$$\end{document}, parallel conjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\wedge}}$$\end{document}, parallel disjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\vee}}$$\end{document}, 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. (shrink)

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , 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.

Within the program of finding axiomatizations for various parts of computability logic, it was proven earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting’s intuitionistic calculus. That sort of reduction permits unlimited reusage of the computational resource represented by the antecedent. An at least equally basic and natural sort of algorithmic reduction, however, is the one that does not allow such reusage. The present article shows that turning the logic of the first sort of (...) reduction into the logic of the second sort of reduction takes nothing more than just deleting the contraction rule from its Gentzen-style axiomatization. The first sort of interactive reduction is also shown to come in three natural versions. While those three versions are very different from each other, their logical behaviors turn out to be indistinguishable, with that common behavior being precisely captured by implicative intuitionistic logic. Among the other contributions of the present article is an informal introduction of a series of new — finite and bounded — versions of recurrence operations and the associated reduction operations. (shrink)