The Parallel versus Branching Recurrences in Computability Logic
Wenyan Xu, Sanyang Liu · Notre Dame Journal of Formal Logic · 2012
This paper shows that the basic logic induced by the parallel recurrence ⅄ \Yup of computability logic (i.e., the one in the signature $\{ ¬, ∧,∨,⅄,\small{𝖸} \}$) is a proper superset of the basic logic induced by the branching recurrence $⫰$ (i.e., the one in the signature $\{ ¬,∧,∨, ⫰, ⫯ \}$). The latter is known to be precisely captured by the cirquent calculus system CL15, conjectured by Japaridze to remain sound—but not complete—with $⅄$ instead of $⫰$. The present result is obtained by positively verifying that conjecture. A secondary result of the paper is showing that $⅄$ is strictly weaker than $⫰$ in the sense that, while $⫰F$ logically implies $⅄F$, the reverse does not hold.