On Displaying Negative Modalities

Sergey Drobyshevich

DOI: http://dx.doi.org/10.12775/LLP.2017.023


We extend Takuro Onishi’s result on displaying substructural negations by formulating display calculi for non-normal versions of impossibility and unnecessity operators, called regular and co-regular negations, respectively, by Dimiter Vakarelov. We make a number of connections between Onishi’s work and Vakarelov’s study of negation. We also prove a decidability result for our display calculus, which can be naturally extended to obtain decidability results for a large number of display calculi for logics with negative modal operators.


display calculus; bi-intuitionistic logic; negative modalities; unnecessity; impossibility; decidability; distributive logic

Full Text:



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

Belnap, N.D., “The display problem”, pages 79–92 in H. Wansing (ed.), Proof Theory of Modal Logic, Applied Logic Series 2, Springer 1996, DOI: 10.1007/978-94-017-2798-3_6

Božić, M., and K. Došen, “Models for normal intuitionistic modal logics”, Studia Logica 43 (1984): 217–245. DOI: 10.1007/BF02429840

Curry, H.B., Foundations of Mathematical Logic, Dover Publications, 1963.

Došen, K., “Negative modal operators in intuitionistic logic”, Publication de l’Instutute Mathematique, Nouv. Ser. 35 (1984): 3–14.

Došen, K., “Negation as a modal operator”, Reports on Mathematical Logic 20 (1986): 15–28.

Drobyshevich, S.A., and S.P. Odintsov, “Finite model property for negative modalities”, Siberian Electronic Mathematical Reports 10 (2013): 1–21 (in Russian). DOI: 10.17377/semi.2013.10.001

Drobyshevich, S., “On classical behavior of intuitionistic modalities”, Logic and Logical Philosophy 24, 1 (2015): 79–104. DOI: 10.12775/LLP.2014.019

Dunn, J.M., “Gaggle theory: An abstraction of Galois connections and residuation with applications to negation, implication, and various logical operators”, pages 31–51 in J. van Eijck (ed.), Logics in AI: European Workshop JELIA ’90, Lecture Notes in Computer Science 478, Springer, Berlin, 1990. DOI: 10.1007/BFb0018431

Dunn, J.M., “Star and perp: Two treatments of negation”, Philosophical Perspectives 7 (1993): 331–357. DOI: 10.2307/2214128

Dunn, J.M., ‘Positive modal logic’, Studia Logica 55, 2 (1995): 301–317. DOI: 10.1007/BF01061239

Dunn, J.M., “Generalized ortho negation”, pages 3–26 in H. Wansing (ed.), Negation: A Notion in Focus, Walter de Gruyter, Berlin, 1996. DOI: 10.1515/9783110876802.3

Dunn, J.M., C. Zhou, “Negation in the context of gaggle theory”, Studia Logica 80 (2005): 235–264. DOI: s11225-005-8470-y

Fischer Servi, G., “On modal logics with an intuitionistic base”, Studia Logica 36 (1977): 141–149. DOI: 10.1007/BF02121259

Fischer Servi, G., “Semantics for a class of intuitionistic modal calculi”, pages 59–72 in: M.L. Dalla Chiara (ed.), Italian Studies in the Philosophy of Science, Vol. 47, Reidel, Dordrecht, 1980. DOI: 10.1007/978-94-009-8937-5_5

Fischer Servi, G., “Axiomatizations for some intuitionistic modal logics”, Rend. Sem. Mat. Univers. Polit. 42 (1984): 179–194.

Goré, R., “Solving the Display Problem via Residuation”, technical report, Automated Reasoning Project Research School of Information Sciences and Engineering and Centre for Information Science Research Australian National University, 1995.

Goré, R., “A uniform display system for intuitionistic and dual intuitionistic logic”, technical report, Automated Reasoning Project TR-ARP-6-95, Australian Nat. Uni., 1995.

Goré, R., “Dual Intuitionistic Logic Revisited”, pages 252–267 in: R. Dyckhoff (ed.), TABLEAUX 2000, Automated Reasoning with Analytic Tableaux and Related Methods, Springer Lecture Notes in AI 1847, Springer Verlag, Berlin, 2000. DOI: 10.1007/10722086_21

Kracht, M., “Power and weakness of the modal display calculus”, pages 93–121 in H. Wansing (ed.), Proof Theory of Modal Logic, Part II, Applied Logic Series, Vol. 2. Springer Netherlands, 1996. DOI: 10.1007/978-94-017-2798-3_7

Odintsov, S.P., Constructive Negations and Paraconsistency, vol. 26 of “Trends in Logic 26”, Springer Netherlands, 2008. DOI: 10.1007/978-1-4020-6867-6

Odintsov, S.P., “Combining intuitionistic connectives and Routley negation”, Siberian Electronic Mathematical Reports 7 (2010): 21–41.

Odintsov, S.P., and H. Wansing, “Constructive predicate logic and constructive modal logic. Formal duality versus semantical duality”, pages 269–286 in: V.F. Hendriks et al. (eds.), First-Order Logic Revisited, Logos Verlag, 2004.

Onishi, T., “Substructural negations”, The Australasian Journal of Logic 12, 4 (2015): 177–203.

Rauszer, C., “A formalization of the propositional calculus of H-B logic”, Studia Logica 33 (1974): 23–34. DOI: 10.1007/BF02120864

Rauszer, C., “Applications of Kripke models to Heyting-Brouwer logic”, Studia Logica 36 (1977): 61–72. DOI: 10.1007/BF02121115

Rauszer, C., An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, Dissertationes Mathematicae 167, 1980. Institute of Mathematics, Polish Academy of Sciences, Warsaw, 62 pp.

Restall, G., “Display logic and gaggle theory”, technical report, Reports on Mathematical Logic, 1995.

Restall, G., “Displaying and deciding substructural logics 1: Logics with contraposition”, Journal of Philosophical Logic 27, 2 (1998): 179–216. DOI: 10.1023/A:1017998605966s

Schmidt, R.A., J.G. Stell, and D. Rydeheard, ‘A bi-intuitionistic modal logic: Foundations and automation’, Journal of Logical and Algebraic Methods in Programming, 85, 4 (2016): 500–519. DOI: 10.1016/j.jlamp.2015.11.003

Shramko, Y., “Dual intuitionistic logic and a variety of negations: The logic of scientific research’, Studia Logica 80, 2–3 (2005), 347–367. DOI: 10.1007/s11225-005-8474-7

Simpson, A., “The proof theory and semantics of intuitionistic modal logic”, PhD dissertation, University of Edinburgh, 1994.

Sotirov, V., “Modal theories with intuitionistic logic”, pages 139–171 in Mathematical Logic. Proc. of the Conference Dedicated to the memory of A.A. Markov (1903–1979), Sofia, September 22–23, Bulgarian Acad. of Sc. 1984.

Sylvan, R., “Variations on Da Costa C systems and dual-intuitionistic logics I. Analyses of C and CC”, Studia Logica 49 (1990): 47–65. DOI: 10.1007/BF00401553

Vakarelov, D., ‘Consistency, completeness and negation’, pages 328–363 in G. Priest, R. Routley, and J. Norman (eds.), Paraconsistent Logics: Essays on the Inconsistent, Filosophia, 1989.

Wansing, H., Displaying Modal Logic, Trends in Logic 3, Kluwer, 1998. DOI: 10.1007/978-94-017-1280-4

Wansing, H., “Constructive negation, implication, and co-implication”, Journal of Applied Non-Classical Logics, 18, 2–3 (2008), 341–364. DOI: 10.3166/jancl.18.341-364

Wansing, H., (2013), ‘Falsification, natural deduction and bi-intuitionistic logic’, Journal of Logic and Computation 26, 1 (2016): 425–450. DOI: 10.1093/logcom/ext035

Wolter, F., and M. Zakharaschev, “Intuitionistic modal logics”, pages 227–238 in A. Cantini, E. Casari, and P. Minari (eds.), Logical Foundations of Mathematics, Synthese Library, Kluwer, 1999. DOI: 10.1007/978-94-017-2109-7_17

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism