The parallel versus branching recurrences in computability logic (Q1934954)

Computability logic ( CoL) is a formal theory of interactive computational problems understood as games between a machine and its environment. CoL has a game semantics. The signature of CoL is \(\mathrm{SU} =(\neg,\wedge,\vee,\downarrow,\uparrow)\), where \(\neg,\wedge,\vee\) are ordinary logical operators and \(\downarrow,\uparrow\) are operators of \textit{uncountable branching recurrence}. If \(F\) is a formula in signature SU, then the formula \(\uparrow F=\neg\downarrow\neg F\) is dual for the formula \(\downarrow F\). The \textit{basic logic} in signature SU (BLinSU) is the set of all formulas in signature SU. \(\mathbf{CL15}\) is a sound and complete axiomatization for the basic (\(\neg,\wedge,\vee,\downarrow,\uparrow\))-fragment of computability logic. \(\mathbf{CL15}\) is a system built in cirquent calculus. Resource semantics are described. The parallel recurrence \(\curlywedge\) and its dual \(\curlyvee\) are considered for which \(\curlyvee F =\neg\curlywedge\neg F\). Three statements are proved. Theorem 1. The basic logic in the signature (\(\neg,\wedge,\vee,\curlywedge,\curlyvee\)) is a proper superset of the basic logic in the signature (\(\neg,\wedge,\vee,\downarrow,\uparrow\)). Theorem 2. The axiomatic system \(\mathbf{CL15}\) with \(\curlywedge,\curlyvee\) instead of \(\downarrow,\uparrow\) is sound but not complete (a conjecture of Japaridze). Theorem 3. The operator \(\curlywedge\) is strictly weaker than \(\downarrow\), that is, \(\downarrow F\) logically implies \(\curlywedge F\), but the reverse does not hold.