The parallel versus branching recurrences in computability logic. (English) Zbl 1291.03072

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 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 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.


03B70 Logic in computer science
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
91A80 Applications of game theory
Full Text: DOI arXiv Euclid


[1] Japaridze, G., “Introduction to computability logic,” Annals of Pure and Applied Logic , vol. 123 (2003), pp. 1-99. · Zbl 1028.03025
[2] Japaridze, G., “Introduction to cirquent calculus and abstract resource semantics,” Journal of Logic and Computation , vol. 16 (2006), pp. 489-532. · Zbl 1113.03023
[3] Japaridze, G., “The logic of interactive Turing reduction,” Journal of Symbolic Logic , vol. 72 (2007), pp. 243-76. · Zbl 1161.03015
[4] Japaridze, G., “Cirquent calculus deepened,” Journal of Logic and Computation , vol. 18 (2008), pp. 983-1028. · Zbl 1170.03028
[5] Japaridze, G., “In the beginning was game semantics,” pp. 249-350 in Games: Unifying Logic, Language, and Philosophy , edited by O. Majer, A.-V. Pietarinen, and T. Tulenheimo, vol. 15 of Logic, Epistemology, and the Unity of Science , Springer, New York, 2009. · Zbl 1171.03015
[6] Japaridze, G., “Many concepts and two logics of algorithmic reduction,” Studia Logica 91 (2009), pp. 1-24. · Zbl 1162.03016
[7] Japaridze, G., “From formulas to cirquents in computability logic,” Logical Methods in Computer Science , vol. 7 (2011), paper 2:1. · Zbl 1218.03026
[8] Japaridze, G., “A new face of the branching recurrence of computability logic,” Applied Mathematics Letters , vol. 25 (2012), pp. 1585-9. DOI · Zbl 1259.03045
[9] Japaridze, G., “Separating the basic logics of the basic recurrences,” Annals of Pure and Applied Logic , vol. 163 (2012), pp. 377-89. · Zbl 1241.03025
[10] Japaridze, G., “The taming of recurrences in computability logic through cirquent calculus, Part I,” preprint, [cs.LO] 1105.3853v4 · Zbl 1298.03068
[11] Japaridze, G., “The taming of recurrences in computability logic through cirquent calculus, Part II,” preprint, [cs.LO] 1106.3705v1 · Zbl 1323.03021
[12] Mezhirov, I., and N. Vereshchagin, “On abstract resource semantics and computability logic,” Journal of Computer and System Sciences , vol. 76 (2010), pp. 356-72. · Zbl 1202.03041
[13] Xu, W., and S. Liu, “Deduction theorem for symmetric cirquent calculus,” pp. 121-26 in Quantitative Logic and Soft Computing 2010 , vol. 82 of Advances in Intelligent and Soft Computing , Springer, Berlin, 2010. · Zbl 1253.03062
[14] Xu, W., and S. Liu, “Soundness and completeness of the cirquent calculus system CL6 for computability logic,” Logic Journal of the IGPL , vol. 20 (2012), pp. 317-30. · Zbl 1258.03033
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.