On a multilattice analogue of a hypersequent S5 calculus

Oleg Grigoriev; Yaroslav Petrukhin

doi:10.12775/LLP.2019.031

Autor

Oleg Grigoriev Lomonosov Moscow State University, Department of Logic, Faculty of Philosophy
Yaroslav Petrukhin Lomonosov Moscow State University,Department of Logic, Faculty of Philosophy

DOI:

https://doi.org/10.12775/LLP.2019.031

Słowa kluczowe

multilattice logic, modal logic, hypersequent calculus, cut elimination, Hilbert-style calculus, embedding theorem, interpolation theorem, generalized truth values

Abstrakt

In this paper, we present a logic MML^S5_n which is a combination of multilattice logic and modal logic S5. MML^S5_n is an extension of Kamide and Shramko’s modal multilattice logic which is a multilattice analogue of S4. We present a cut-free hypersequent calculus for MML^S5_n in the spirit of Restall’s one for S5 and develop a Kripke semantics for MML^S5_n, following Kamide and Shramko’s approach. Moreover, we prove theorems for embedding MML^S5_n into S5 and vice versa. As a result, we obtain completeness, cut elimination, decidability, and interpolation theorems for MML^S5_n. Besides, we show the duality principle for MML^S5_n. Additionally, we introduce a modification of Kamide and Shramko’s sequent calculus for their multilattice version of S4 which (in contrast to Kamide and Shramko’s original one) proves the interdefinability of necessity and possibility operators. Last, but not least, we present Hilbert-style calculi for all the logics in question as well as for a larger class of modal multilattice logics.

Bibliografia

Arieli, O., Avron, A., “Reasoning with logical bilattices”, Journal of Logic, Language and Information 5 (1996): 25–63. DOI: http://dx.doi.org/10.1007/BF00215626

Avron, A., “A constructive analysis of RM”, Journal of Symbolic Logic 52, 4 (1987): 939–951. DOI: http://dx.doi.org/10.2307/2273828

Avron, A., “The method of hypersequents in the proof theory of propositional non-classical logic”, pages 1–32 in Logic: from Foundations to Applications, 1996.

Bednarska, K., and A. Indrzejczak, “Hypersequent calculi for S5: The methods of cut elimination”, Logic and Logical Philosophy 24, 3 (2015): 277–311. DOI: http://dx.doi.org/10.12775/LLP.2015.018

Belnap, N.D., “A useful four-valued logic”, pages 7–37 in J.M. Dunn and G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, Boston: Reidel Publishing Company, 1977. DOI: http://dx.doi.org/10.1007/978-94-010-1161-7_2

Belnap, N.D., “How a computer should think”, pages 30–56 in G. Rule (ed.), Contemporary Aspects of Philosophy, Stocksfield: Oriel Press, 1977.

Belnap, N.D., “Display logic”, Journal of Philosophical Logic 11, 4 (1982): 375–417. DOI: http://dx.doi.org/10.1007/BF00284976

Braüner, T., “A cut-free Gentzen formulation of the modal logic S5”, Logic Journal of the IGPL 8, 5 (2000): 629–643. DOI: http://dx.doi.org/10.1093/jigpal/8.5.629

Chagrov A., and M. Zakharyaschev, Modal Logic, Oxford Logic Guide, vol. 35, Oxford University Press, 1997.

Chellas, B.F., Modal Logic. An Introduction, Cambridge University Press, 1980. DOI: http://dx.doi.org/10.1017/CBO9780511621192

Degauquier, V., “A useful four-valued extension of the temporal logic KtT4”, Bulletin of the Section of Logic 47 (2018): 15–31. DOI: http://dx.doi.org/10.18778/0138-0680.47.1.02

Dunn, J.M., “Intuitive semantics for first-degree entailment and coupled trees”, Philosophical Studies 29 (1976): 149-168. DOI: http://dx.doi.org/10.1007/BF00373152

Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel: Dordrecht, 1983.

Fitting, M.,“Many-valued modal logics”, Fundamenta Informaticae 15 (1991): 235–254.

Fitting, M.: “Many-valued modal logics II”, Fundamenta Informaticae 17 (1992): 55–73.

Ginsberg, M., “Multi-valued logics”, pages 243–247 in Proceedings of AAAI-86, Fifth National Conference on Artificial Intellegence, Morgan Kaufman Publishers, Los Altos, 1986.

Ginsberg, M., “Multivalued logics: a uniform approach to reasoning”, Computational Intelligence 4, 3 (1988): 265–316. DOI: http://dx.doi.org/10.1111/j.1467-8640.1988.tb00280.x

Goble, L., “Paraconsistent modal logic”, Logique et Analyse 49 (2006): 3–29.

Grigoriev, O., and Y. Petrukhin, “Two proofs of the algebraic completeness theorem for multilattice logic”, submitted.

Indrzejczak, A., “Cut-free double sequent calculus for S5”, Logic Journal of the IGPL 6, 3 (1998): 505–516. DOI: http://dx.doi.org/10.1093/jigpal/6.3.505

Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics, Springer, 2010.

Indrzejczak, A., “Cut-free hypersequent calculus for S4.3”, Bulletin of the Section of Logic 41, 1/2 (2012): 89–104.

Indrzejczak, A., “Eliminability of cut in hypersequent calculi for some modal logics of linear frames”, Information Processing Letters 115, 2 (2015): 75–81. DOI: http://dx.doi.org/10.1016/j.ipl.2014.07.002

Indrzejczak, A., “Linear time in hypersequent framework”, The Bulletin of Symbolic Logic 22, 1 (2016): 121–144. DOI:

Indrzejczak, A., “Cut elimination theorem for non-commutative hypersequent calculus”, Bulletin of the Section of Logic 46, 1/2 (2017): 135–149. DOI: http://dx.doi.org/10.18778/0138-0680.46.1.2.10

Kamide, N., “Phase Semantics for Multilattice Formalism”, IEEE 47th International Symposium on Multiple-Valued Logic, 2017. DOI: http://dx.doi.org/10.1109/ISMVL.2017.13

Kamide, N., and Y. Shramko, “Embedding from multilattice logic into classical logic and vice versa”, Journal of Logic and Computation 27, 5 (2017): 1549–1575. DOI: http://dx.doi.org/10.1093/logcom/exw015

Kamide, N., and Y. Shramko, “Modal multilattice logic”, Logica Universalis 11, 3 (2017): 317–343. DOI: http://dx.doi.org/10.1007/s11787-017-0172-5

Kamide, N., Y. Shramko, and H. Wansing, “Kripke completeness of biintuitionistic multilattice logic and its connexive variant”, Studia Logica 105, 5 (2017): 1193–1219. DOI: http://dx.doi.org/10.1007/s11225-017-9752-x

Kanger, S., “Provability in logic”, Stockholm Studies in Philosophy, series “Acta Universitatis Stockholmiensis”, Almqvist and Wiskell: Stockholm, 1957.

Kripke, S., “Semantical analysis of modal logic I”. Zeitschrif t für Mathematische Logik und Grundlegen der Mathematik 9 (1963): 67–96.

Kurokawa, H., “Hypersequent calculi for modal logics extending S4”, pages 51–68 in New Frontiers in Artificial Intelligence, series “Lecture Notes in Computer Science”, 2013. DOI: http://dx.doi.org/10.1007/978-3-319-10061-6_4

Lahav, O., “From frame properties to hypersequent rules in modal logics”, pages 408–417 in 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013. DOI: http://dx.doi.org/10.1109/LICS.2013.47

Mints, G., “Cut-free calculi of the S5 typeâĂİ, pages 79–82 in Studies in Constructive Mathematics and Mathematical Logic, part 2, 1970. DOI: http://dx.doi.org/10.1007/978-1-4899-5327-8_16

Negri, S., “Proof analysis in modal logic”, Journal of Philosophical Logic 34, 5–6 (2005): 507–544. DOI: http://dx.doi.org/10.1007/s10992-005-2267-3

Odintsov, S.P., and E.I. Latkin, “BK-lattices. Algebraic semantics for Belnapian modal logics”, Studia Logica 100, 1–2 (2012): 319–338. DOI: http://dx.doi.org/10.1007/s11225-012-9380-4

Odintsov, S.P., D. Skurt, H. Wansing, “On Definability of connectives and modal logics over FDE”, Logic and Logical Philosophy (2019). DOI: href="http://dx.doi.org/10.12775/LLP.2019.010

Odintsov, S.P., and S. Speranski, “The lattice of Belnapian modal logics: special extensions and counterparts”, Logic and Logical Philosophy 25 (2016): 3–33. DOI: http://dx.doi.org/10.12775/LLP.2016.002

Odintsov, S.P., and S. Speranski, “Belnap-Dunn modal logics: truth constants vs. truth values”, Review of Symbolic Logic (2019). DOI: http://dx.doi.org/10.1017/S1755020319000121

Odintsov, S.P., and H. Wansing, “Modal logics with Belnapian truth values”, Journal of Applied Non-Classical Logics 20 (2010): 279–301. DOI: http://dx.doi.org/10.3166/jancl.20.279-301

Odintsov, S.P., and H. Wansing, “Disentangling FDE-based paraconsistent modal logics”, Studia Logica 105 (2017): 1221–1254. DOI: http://dx.doi.org/10.1007/s11225-017-9753-9

Ohnishi, M., and K. Matsumoto, “Gentzen method in modal calculi I”, Osaka Mathematical Journal 9, 2 (1957): 113–130.

Ohnishi, M., and K. Matsumoto, “Gentzen method in modal calculi II”, Osaka Mathematical Journal 11, 2 (1959): 115–120.

Priest, G., An Introduction to Non-Classical Logic. From If to Is, Cambridge University Press, Cambridge, 2008. DOI: http://dx.doi.org/10.1017/CBO9780511801174

Priest, G., “Many-valued modal logics: a simple approach”, Review of Symbolic Logic 1, 2 (2008): 190–203. DOI: http://dx.doi.org/10.1017/S1755020308080179

Poggiolesi, F., “A cut-free simple sequent calculus for modal logic S5”, Review of Symbolic Logic 1, 1 (2008): 3–15. DOI: http://dx.doi.org/10.1017/S1755020308080040

Pottinger, G., “Uniform cut-free formulations of T, S 4 and S 5 (abstract)”, Journal of Symbolic Logic 48 (1983): 900. DOI: http://dx.doi.org/10.2307/2273495

Restall, G., “Proofnets for S5: Sequents and circuits for modal logic”, pages 151–172 in Logic Colloquium 2005, series “Lecture Notes in Logic”, no. 28, Cambridge University Press, 2007. DOI: http://dx.doi.org/10.1017/CBO9780511546464.012

Rivieccio, U., A. Jung, A., and R. Jansana, “Four-valued modal logic: Kripke semantics and duality”, Journal of Logic and Computation 27 (2017): 155–199. DOI: http://dx.doi.org/10.1093/logcom/exv038

Sato, M., “A study of Kripke-type models for some modal logics by Gentzen’s sequential method”, Publications of the Research Institute for Mathematical Sciences, Kyoto University 13 (1977): 381–468.

Shramko, Y., “Truth, falsehood, information and beyond: the American plan generalized”, pages 191–212 in K. Bimbo (ed.), J. Michael Dunn on Information Based Logics, Outstanding Contributions to Logic, Springer, Dordrecht, 2016. DOI: http://dx.doi.org/10.1007/978-3-319-29300-4_11

Shramko, Y., J.M. Dunn, and T. Takenaka, “The trilattice of constructive truth values”, Journal of Logic and Computation 11, 6 (2001): 761–788. DOI: http://dx.doi.org/10.1093/logcom/11.6.761

Shramko, Y., and H. Wansing, “Some useful sixteen-valued logics: how a computer network should think”, Journal of Philosophical Logic 34 (2005): 121–153. DOI: http://dx.doi.org/10.1007/s10992-005-0556-5

Shramko, Y., and H. Wansing, Truth and Falsehood. An Inquiry into Generalized Logical Values, Springer, Dordrecht, 2011. DOI: http://dx.doi.org/10.1007/978-94-007-0907-2

Sedlár, I., “Propositional dynamic logic with Belnapian truth values”, pages 503–519 in Advances in Modal Logic, vol. 11, 2016.

Stouppa, P., “A deep inference system for the modal logic S5”, Studia Logica 85, 2 (2007): 199–214. DOI: http://dx.doi.org/10.1007/s11225-007-9028-y

Takano, M., “Subformula property as a substitute for cut-elimination in modal propositional logics”, Mathematica Japonica 37, 6 (1992): 1129–1145.

Takano, M., “A modified subformula property for the modal logics K5 and K5D”, Bulletin of the Section of Logic 30, 2 (2001): 115–122.

Zaitsev, D., “A few more useful 8-valued logics for reasoning with tetralattice EIGHT4”, Studia Logica 92, 2 (2009): 265–280. DOI: http://dx.doi.org/10.1007/s11225-009-9198-x