Abstract
Motivated by the interpretation of substructural logics as resource-conscious reasoning, we introduce a client-server game characterizing provability in single-conclusion sequent calculi. The set up is modular and allows to capture multiple logics, including intuitionistic and (affine) linear intuitionistic logic. We also provide a straightforward interpretation of subexponentials, and moreover introduce a game where the information provided by the server is organized as a stack, rather than as a multiset or list.
Funded by FWF projects W1255-N23 and FWF P25417-G15 LOGFRADIG.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Since we only care about winning strategies for \(\mathbf C \), the server \(\mathbf S \) may be viewed as acting nondeterministically or probabilistically, if preferred.
- 2.
\(\bigwedge \varGamma \) denotes the conjunction of all formulas in \(\varGamma \).
- 3.
We assume that \(\mathbf {LI}\) is already formulated using multisets - otherwise, this would be another difference between the calculi.
- 4.
In these rules, the operations of replacing and removing an ip in a multiset are meant to affect only the active instance of the ip, rather than all instances of the ip in the multiset.
- 5.
We remark that (W) is not admissible in \(\mathbf {IAL}\), even if one relaxes the axioms, because of the (!R)-rule. Our corresponding (\(\text {C}\textsc {heck}\) !F)-rule is different: It could be written as
which has a built-in weakening.
- 6.
We remark that the combination of the rules (!C), (!dR) and (!R\(^\omega \)) does define an exponential ! uniquely. However, cut is not admissible in the resulting system.
References
Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. J. Symb. Log. 59(02), 543–574 (1994)
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)
Blass, A.: A game semantics for linear logic. Ann. Pure Appl. Log. 56(1), 183–220 (1992)
Danos, V., Joinet, J.-B., Schellinx, H.: The structure of exponentials: uncovering the dynamics of linear logic proofs. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol. 713, pp. 159–171. Springer, Heidelberg (1993). doi:10.1007/BFb0022564
Girard, J.-Y.: Linear logic: its syntax and semantics. In: Advances in linear logic (Ithaca, NY, 1993). London Mathematical Society Lecture Note Series, vol. 222, pp. 1–42. Cambridge University Press, Cambridge (1995)
Japaridze, G.: The intuitionistic fragment of computability logic at the propositional level. Ann. Pure Appl. Log. 147(3), 187–227 (2007)
Keiff, L.: Dialogical logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2011 edition (2011)
Lafont,Y., Streicher, T.: Games semantics for linear logic. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, LICS 1991, pp. 43–50. IEEE (1991)
Lorenzen, P.: Logik und Agon. In: Atti del XII Congresso Internazionale di Filosofia, vol. 4, pp. 187–194 (1960)
Paoli, F.: Substructural Logics: A Primer. Springer, Heidelberg (2013)
Rahman, S., Rückert, H.: Dialogical connexive logic. Synthese 127(1), 105–139 (2001)
Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. Cambridge Tracts in Theoretical Computer Science, vol. 43, 2nd edn. Cambridge University Press, Cambridge (2000)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Fermüller, C.G., Lang, T. (2017). Interpreting Sequent Calculi as Client-Server Games. In: Schmidt, R., Nalon, C. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2017. Lecture Notes in Computer Science(), vol 10501. Springer, Cham. https://doi.org/10.1007/978-3-319-66902-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-66902-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66901-4
Online ISBN: 978-3-319-66902-1
eBook Packages: Computer ScienceComputer Science (R0)