Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-23T09:21:38.909Z Has data issue: false hasContentIssue false
  • English
  • Français

KRIPKE COMPLETENESS OF STRICTLY POSITIVE MODAL LOGICS OVER MEET-SEMILATTICES WITH OPERATORS

Published online by Cambridge University Press:  03 April 2019

STANISLAV KIKOT ,
AGI KURUCZ ,
YOSHIHITO TANAKA ,
FRANK WOLTER  and
MICHAEL ZAKHARYASCHEV
STANISLAV KIKOT
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF OXFORD WOLFSON BUILDING, PARKS ROAD, OXFORD OX1 3QD, UK and DEPARTMENT OF COMPUTER SCIENCE AND INFORMATION SYSTEMS BIRKBECK, UNIVERSITY OF LONDON MALET STREET, LONDON WC1E 7HX, UK and INSTITUTE FOR INFORMATION TRANSMISSION PROBLEMS 19 BOLSHOY KARETNY PEREULOK, MOSCOW 127051, RUSSIA and MOSCOW INSTITUTE OF PHYSICS AND TECHNOLOGY 9 INSTITUTSKIY PEREULOK, DOLGOPRUDNY, MOSCOW REGION141701, RUSSIAE-mail: [email protected]
AGI KURUCZ
Affiliation:
DEPARTMENT OF INFORMATICS KING’S COLLEGE LONDON STRAND CAMPUS, BUSH HOUSE, 30 ALDWYCH, LONDON WC2B 4BG, UK E-mail: [email protected]
YOSHIHITO TANAKA
Affiliation:
FACULTY OF ECONOMICS KYUSHU SANGYO UNIVERSITY 2-3-1 MATSUKADAI, HIGASHI-KU, FUKUOKA813-8503, JAPANE-mail: [email protected]
FRANK WOLTER
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF LIVERPOOL ASHTON BUILDING, ASHTON STREET, LIVERPOOL L69 3BX, UK E-mail: [email protected]
MICHAEL ZAKHARYASCHEV
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE AND INFORMATION SYSTEMS BIRKBECK, UNIVERSITY OF LONDON MALET STREET, LONDON WC1E 7HX, UK E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic.

Keywords

03B4503G25semilattices with operatorsmodal logicKripke completeness
Type
Articles
Information
The Journal of Symbolic Logic , Volume 84 , Issue 2 , June 2019 , pp. 533 - 588
Copyright
Copyright © The Association for Symbolic Logic 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Allwein, G. and Dunn, J., Kripke models for linear logic, this Journal, vol. 58 (1993), pp. 514–545.Google Scholar
Baader, F., Restricted role-value-maps in a description logic with existential restrictions and terminological cycles, Proceedings of the 2003 International Workshop on Description Logics (DL2003) (Calvanese, D., De Giacomo, G., and Franconi, E., editors), CEUR Workshop Proceedings, vol. 81, CEUR-WS.org, Aachen, Germany, 2003.Google Scholar
Baader, F., Brandt, S., and Lutz, C., Pushing the ${\cal E}{\cal L}$ envelope, Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI-2005) (Kaelbling, L. P. and Saffiotti, A., editors), Professional Book Center, San Francisco, CA, 2005, pp. 364–369.Google Scholar
Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., and Patel-Schneider, P. F. (eds.), The Description Logic Handbook: Theory, Implementation, and Applications, Cambridge University Press, Cambridge, 2003.Google Scholar
Baader, F., Horrocks, I., Lutz, C., and Sattler, U., An Introduction to Description Logic, Cambridge University Press, Cambridge, 2017.Google Scholar
Baader, F., Küsters, R., and Molitor, R., Computing least common subsumers in description logics with existential restrictions, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI’99) (Dean, T., editor), Morgan Kaufmann, Burlington, MA, 1999, pp. 96–101.Google Scholar
Beklemishev, L., Calibrating provability logic: From modal logic to reflection calculus, Advances in Modal Logic, vol. 9 (Bolander, T., Braüner, T., Ghilardi, S., and Moss, L., editors), College Publications, London, 2012, pp. 89–94.Google Scholar
Beklemishev, L., Positive provability logic for uniform reflection principles. Annals of Pure and Applied Logic, vol. 165 (2014), pp. 82–105.Google Scholar
Beklemishev, L., Personal communication, 2015.Google Scholar
Beklemishev, L., On the reflection calculus with partial conservativity operators, Proceedings of the 24th Workshop on Logic, Language, Information, and Computation (WoLLIC 2017) (Kennedy, J. and de Queiroz, R., editors), Springer, Berlin, 2017, pp. 48–67.Google Scholar
Beklemishev, L., A note on strictly positive logics and word rewriting systems, Larisa Maksimova on Implication, Interpolation, and Definability (Odintsov, S., editor), Outstanding Contributions to Logic, vol. 15, Springer, Berlin, 2018, pp. 61–70.Google Scholar
Birkhoff, G., On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society, vol. 31 (1935), pp. 433–454.Google Scholar
Blackburn, P., de Rijke, M., and Venema, Y., Modal Logic, Cambridge University Press, Cambridge, 2001.Google Scholar
Blackburn, P., van Benthem, J., and Wolter, F. (eds.), Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, Elsevier, Amsterdam, 2007.Google Scholar
Blok, W., On the degree of incompleteness in modal logics and the covering relation in the lattice of modal logics, Technical Report 78-07, 1978, Department of Mathematics, University of Amsterdam.Google Scholar
Boolos, G., The Logic of Provability, Cambridge University Press, Cambridge, 1995.Google Scholar
Celani, S. and Jansana, R., A new semantics for positive modal logic. Notre Dame Journal of Formal Logic, vol. 38 (1997), pp. 1–18.Google Scholar
Celani, S. and Jansana, R., Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic. Logic Journal of the IGPL, vol. 7 (1999), pp. 683–715.Google Scholar
Chagrov, A. and Chagrova, L., The truth about algorithmic problems in correspondence theory, Advances in Modal Logic, vol. 6 (Governatori, G., Hodkinson, I., and Venema, Y., editors), College Publications, London, 2006, pp. 121–138.Google Scholar
Chagrov, A. and Shehtman, V., Algorithmic aspects of propositional tense logics, Proceedings of the 8th Workshop on Computer Science Logic (CSL’94) (Pacholski, L. and Tiuryn, J., editors), LNCS, vol. 933, Springer, Berlin, 1995, pp. 442–455.Google Scholar
Chagrov, A. and Zakharyaschev, M., The undecidability of the disjunction property of propositional logics and other related problems, this Journal, vol. 58 (1993), pp. 967–1002.Google Scholar
Chagrov, A. and Zakharyaschev, M., Modal Logic, Oxford Logic Guides, vol. 35, Clarendon Press, Oxford, 1997.Google Scholar
Chang, C. C. and Keisler, H. J., Model Theory, North-Holland, Amsterdam, 1973.Google Scholar
Dantsin, E., Eiter, T., Gottlob, G., and Voronkov, A., Complexity and expressive power of logic programming. ACM Computing Surveys, vol. 33 (2001), no. 3, pp. 374–425.Google Scholar
Dashkov, E., On the positive fragment of the polymodal provability logic GLP. Mathematical Notes, vol. 91 (2012), pp. 318–333.Google Scholar
Davey, B. A., Jackson, M., Pitkethly, J. G., and Talukder, M. R., Natural dualities for semilattice-based algebras. Algebra Universalis, vol. 57 (2007), pp. 463–490.Google Scholar
Davis, M. D., Computability and Unsolvability, McGraw-Hill Series in Information Processing and Computers, McGraw-Hill, New York, 1958.Google Scholar
Donini, F., Hollunder, B., Lenzerini, M., Nardi, D., Nutt, W., and Spaccamela, A., The complexity of existential quantification in concept languages. Artificial Intelligence, vol. 53 (1992), pp. 309–327.Google Scholar
Dunn, J., Positive modal logic. Studia Logica, vol. 55 (1995), pp. 301–317.Google Scholar
Fariñas del Cerro, L. and Penttonen, M. Grammar logics. Logique et Analyse, vol. 121–122 (1988), pp. 123–134.Google Scholar
Fine, K., An ascending chain of S4 logics . Theoria , vol. 40 (1974), pp. 110–116.Google Scholar
Fine, K., An incomplete logic containing S4. Theoria, vol. 40 (1974), pp. 23–29.Google Scholar
Gehrke, M. and Harding, J., Bounded lattice expansions. Journal of Algebra, vol. 238 (2001), pp. 345–371.Google Scholar
Gehrke, M. and Jónsson, B., Bounded distributive lattices with operators. Mathematica Japonica, vol. 40 (1994), pp. 207–215.Google Scholar
Gehrke, M. and Jónsson, B., Monotone bounded distributive lattice expansions. Mathematica Japonica, vol. 52 (2000), pp. 197–213.Google Scholar
Gehrke, M. and Jónsson, B., Bounded distributive lattice expansions. Mathematica Scandinavica, vol. 94 (2004), pp. 3–45.Google Scholar
Gehrke, M., Nagahashi, H., and Venema, Y., A Sahlqvist theorem for distributive modal logic. Annals of Pure and Applied Logic, vol. 131 (2005), pp. 65–102.Google Scholar
Ghilardi, S. and Meloni, G., Constructive canonicity in nonclassical logics. Annals of Pure and Applied Logic, vol. 86 (1997), pp. 1–32.Google Scholar
Goldblatt, R., Metamathematics of modal logic, Part I. Reports on Mathematical Logic, vol. 6 (1976), pp. 41–78.Google Scholar
Goldblatt, R., Varieties of complex algebras. Annals of Pure and Applied Logic, vol. 44 (1989), pp. 173–242.Google Scholar
Goldblatt, R. and Thomason, S., Axiomatic classes in propositional modal logic, Algebra and Logic (Crossley, J., editor), Lecture Notes in Mathematics, vol. 450, Springer, Berlin, 1974, pp. 163–173.Google Scholar
Grätzer, G., Universal Algebra, second ed., Springer, Berlin, 1979.Google Scholar
Hartonas, C. and Dunn, J., Stone duality for lattices. Algebra Universalis, vol. 37 (1997), pp. 391–401.Google Scholar
Hemaspaandra, E., The complexity of poor man’s logic. Journal of Logic and Computation, vol. 11 (2001), pp. 609–622.Google Scholar
Hemaspaandra, E. and Schnoor, H., On the complexity of elementary modal logics, Proceedings of the 25th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2008) (Albers, S. and Weil, P., editors), Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2008, pp. 349–360.Google Scholar
Jackson, M., Semilattices with closure. Algebra Universalis, vol. 52 (2004), pp. 1–37.Google Scholar
Jankov, V. A., The relationship between deducibility in the intuitionistic propositional calculus and finite implicational structures. Soviet Mathematics Doklady, vol. 4 (1963), pp. 1203–1204.Google Scholar
Japaridze, G. K., The modal-logical means of studying provability, Ph.D. thesis, Moscow, 1986, (in Russian).Google Scholar
Jónsson, B. and Tarski, A., Boolean algebras with operators. I. American Journal of Mathematics, vol. 73 (1951), pp. 891–939.Google Scholar
Kikot, S., On modal definability of Horn formulas, Proceedings of the 5th International Conference on Topology, Algebra and Categories in Logic (TACL-2011) (Santocanale, L., Olevetti, N., and Lafont, Y., editors), Marseille, France, 2011, pp. 175–178.Google Scholar
Kikot, S., Kurucz, A., Wolter, F., and Zakharyaschev, M., On strictly positive modal logics with S4.3 frames, Advances in Modal Logic, vol. 12 (Bezhanishvili, G., D’Agostino, G., Metcalfe, G., and Studer, T., editors), College Publications, London, 2018, pp. 399–418.Google Scholar
Kikot, S., Shapirovsky, I., and Zolin, E., Filtration safe operations on frames, Advances in Modal Logic, vol. 10 (Goré, R., Kooi, B., and Kurucz, A., editors), College Publications, London, 2014, pp. 333–352.Google Scholar
Kracht, M., Modal consequence relations, Handbook of Modal Logic (Blackburn, P., van Benthem, J., and Wolter, F., editors), Studies in Logic and Practical Reasoning, vol. 3, Elsevier, Amsterdam, 2007, pp. 491–545.Google Scholar
Kurucz, A., Wolter, F., and Zakharyaschev, M., Islands of tractability for relational constraints: Towards dichotomy results for the description logic ${\cal E}{\cal L}$., Advances in Modal Logic, vol. 8 (Beklemishev, L., Goranko, V., and Shehtman, V., editors), College Publications, London, 2010, pp. 271–291.Google Scholar
Litak, T., Stability of the Blok theorem. Algebra Universalis, vol. 58 (2008), pp. 385–411.Google Scholar
Lutz, C. and Wolter, F., Mathematical logic for life science ontologies, Proceedings of the 16th Workshop on Logic, Language, Information, and Computation (WoLLIC 2009) (Ono, H., Kanazawa, M., and de Queiroz, R., editors), LNCS, vol. 5514, Springer, Berlin, 2009, pp. 37–47.Google Scholar
McKenzie, R., Tarski’s finite basis problem is undecidable. International Journal of Algebra and Computation, vol. 6 (1996), pp. 49–104.Google Scholar
McKinsey, J. C. C. and Tarski, A., The algebra of topology. Annals of Mathematics, vol. 45 (1944), pp. 141–191.Google Scholar
Michaliszyn, J. and Otop, J., Decidable elementary modal logics, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS’12) (Dershowitz, N., editor), IEEE Computer Society, Los Alamitos, CA, 2012, pp. 491–500.Google Scholar
http://www.w3.org/TR/owl2-overview/.Google Scholar
Priestley, H., Representations of distributive lattices by means of ordered Stone spaces. Bulletin of the London Mathematical Society, vol. 2 (1970), pp. 186–190.Google Scholar
Rasiowa, H. and Sikorski, R., The Mathematics of Metamathematics, Polish Scientific Publishers, Warsaw, 1963.Google Scholar
Sahlqvist, H., Completeness and correspondence in the first- and second-order semantics for modal logic, Proceedings of the 3rd Scandinavian Logic Symposium (Kanger, S., editor), North-Holland, Amsterdam, 1975, pp. 110–143.Google Scholar
Schmidt-Schauss, M. and Smolka, G., Attributive concept descriptions with complements. Artificial Intelligence, vol. 48 (1991), pp. 1–26.Google Scholar
Shapirovsky, I., Pspace-decidability of Japaridze’s polymodal logic, Advances in Modal Logic, vol. 7 (Areces, C. and Goldblatt, R., editors), College Publications, London, 2008, pp. 289–304.Google Scholar
Shehtman, V., Undecidable propositional calculi, Problems in Cybernetics, Non-Classical Logics and their Applications, vol. 75, USSR Academy of Sciences, Moscow, 1982, pp. 74–116.Google Scholar
http://www.ihtsdo.org/snomed-ct.Google Scholar
Sofronie-Stokkermans, V., Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of nonclassical logics I. Studia Logica, vol. 64 (2000), pp. 93–132.Google Scholar
Sofronie-Stokkermans, V., Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of nonclassical logics II. Studia Logica, vol. 64 (2000), pp. 151–172.Google Scholar
Sofronie-Stokkermans, V., Representation theorems and the semantics of (semi)lattice-based logics, Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2001) (Konikowska, B., editor), IEEE Computer Society, Los Alamitos, CA, 2001, pp. 125–136.Google Scholar
Sofronie-Stokkermans, V., Locality and subsumption testing in ${\cal E}{\cal L}$and some of its extensions , Advances in Modal Logic, vol. 7 (Areces, C. and Goldblatt, R., editors), College Publications, London, 2008, pp. 315–339.Google Scholar
Svyatlovskiy, M., Axiomatization and polynomial solvability of strictly positive fragments of certain modal logics. Mathematical Notes, vol. 103 (2018), pp. 952–967.Google Scholar
Thomason, S., An incompleteness theorem in modal logic. Theoria, vol. 40 (1974), pp. 30–34.Google Scholar
Thomason, S., Undecidability of the completeness problem of modal logic, Universal Algebra and Applications, Banach Center Publications, vol. 9, PNW–Polish Scientific Publishers, Warsaw, 1982, pp. 341–345.Google Scholar
Tseitin, G. S., An associative calculus with an insoluble problem of equivalence, Problems of the Constructive Direction in Mathematics. Part 1, Trudy Mat. Inst. Steklov, Acad. Sci. USSR, Steklov Institute of Mathematics, Moscow, 1958, pp. 172–189.Google Scholar
Urquhart, A., A topological representation theory for lattices. Algebra Universalis, vol. 8 (1978), pp. 45–58.Google Scholar
Zakharyaschev, M., Wolter, F., and Chagrov, A., Advanced modal logic, Handbook of Philosophical Logic (Gabbay, D. M. and Guenthner, F., editors), Springer, Berlin, 2001, pp. 83–266.Google Scholar