This paper shows that the basic logic induced by the parallel recurrence $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ of computability logic (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}},\hspace {-2pt}\mbox {\raisebox {0.12cm}{\@setfontsize \small {7}{8}$\vee$}\hspace {-3.6pt}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ) is a proper superset of the basic logic induced by the branching recurrence $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox (...) {3.1pt}{\tiny $\mid$}\hspace {2pt}},\mbox {\raisebox {0.12cm}{$\circ$}\hspace {-0.115cm}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ). The latter is known to be precisely captured by the cirquent calculus system CL15 , conjectured by Japaridze to remain sound—but not complete—with $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ instead of $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ . The present result is obtained by positively verifying that conjecture. A secondary result of the paper is showing that $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ is strictly weaker than $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ in the sense that, while $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}F$ logically implies $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}F$ , the reverse does not hold. (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 \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)