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

### MSC:

 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:

### References:

  Japaridze, G., “Introduction to computability logic,” Annals of Pure and Applied Logic , vol. 123 (2003), pp. 1-99. · Zbl 1028.03025  Japaridze, G., “Introduction to cirquent calculus and abstract resource semantics,” Journal of Logic and Computation , vol. 16 (2006), pp. 489-532. · Zbl 1113.03023  Japaridze, G., “The logic of interactive Turing reduction,” Journal of Symbolic Logic , vol. 72 (2007), pp. 243-76. · Zbl 1161.03015  Japaridze, G., “Cirquent calculus deepened,” Journal of Logic and Computation , vol. 18 (2008), pp. 983-1028. · Zbl 1170.03028  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  Japaridze, G., “Many concepts and two logics of algorithmic reduction,” Studia Logica 91 (2009), pp. 1-24. · Zbl 1162.03016  Japaridze, G., “From formulas to cirquents in computability logic,” Logical Methods in Computer Science , vol. 7 (2011), paper 2:1. · Zbl 1218.03026  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  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  Japaridze, G., “The taming of recurrences in computability logic through cirquent calculus, Part I,” preprint, [cs.LO] 1105.3853v4 · Zbl 1298.03068  Japaridze, G., “The taming of recurrences in computability logic through cirquent calculus, Part II,” preprint, [cs.LO] 1106.3705v1 · Zbl 1323.03021  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  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  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.