The countable versus uncountable branching recurrences in computability logic (Q1948283)

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 to the formula \(\downarrow F\). The basic logic in signature SU (BLinSU) is the set of all formulas in signature SU. A version of the \textit{countable branching recurrence} \(\downarrow^{\aleph}\) and its dual \(\uparrow^{\aleph}\) of computability logic and the basic logic BLinSC in signature \(\mathrm{SC} = (\neg, \wedge, \vee, \downarrow^{\aleph}, \uparrow^{\aleph})\) are introduced. It is shown that the operator \(\downarrow^{\aleph}\) is strictly weaker that \(\downarrow\) in the sense that \(\downarrow F\) logically implies \(\downarrow^{\aleph} F\) but not vice versa. It is shown that the basic logic BLinSC in the signature SC with respect to valididy (relatively to the game semantics) is a proper superset of the basic logic BLinSU. It is known that there is a sound and complete axiomatization CL15(BLinSU) for BLinSU, called cirquent calculus. Here it is proved that the axiomatization CL15(BLinSC) is sound, but not complete. Resource semantics are described.