Abstract
Dyckhoff and Negri (Arch Math Logic 51:71–92 (2012), [8]) give a constructive proof of Gödel–Mckinsey–Tarski embedding from intermediate logics to modal logics via labelled sequent calculi. Then, they regard a monotonicity of atomic propositions in intuitionistic logic as an initial sequent, i.e., an axiom. However, we regard the monotonicity as an additional inference rule and employ a modified translation sending an atomic variable P to \( P \& \Box P\) to generalize their result to an embedding from extensions of Corsi’s \(\mathbf {F}\) of logic of strict implication to normal extensions of modal logics \(\mathbf {K}\). In this process, we provide a \(\mathbf {G3}\)-style labelled sequent calculi for extensions of \(\mathbf {F}\) and show that our calculi admit the cut rule and enjoy soundness and completeness for Kripke semantics.
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
Notes
- 1.
In the last moment of revising this paper, we were informed that Sara Negri [23] also proposed a different translation of ours to obtain a similar result for subintuitionistic logic without the requirement of monotonicity. However, her result did not cover Visser’s basic propositional logic.
- 2.
The revised translation sending P to \( P \& \Box P\) was recently also employed by the second author and Ma [28] for providing a topological semantics for Visser’s basic propositional logic.
- 3.
\(\mathbf {G3}\)-style sequent calculus, which was first developed by Kleene in [15], is the sequent calculus that does not contain any structural rule: rules of weakening, contraction and exchange, while it has an axiom with a context: \(A, \varGamma \Rightarrow \varDelta , A\). In [7], Dragalin showed that rules of weakening and contraction are height-preserving admissible. A general introduction to \(\mathbf {G3}\)-style sequent calculus can be found in [24, 31].
References
Aghaei, M., Ardeshir, M.: A bounded translation of intuitionistic propositional logic into basic propositional logic. Math. Log. Q. 46, 199–206 (2000)
Ardeshir, M., Ruitenburg, W.: Basic propositional calculus I. Math. Log. Q. 44, 317–343 (1998)
Cerrato, C.: Natural deduction based upon strict implication for normal modal logics. Notre Dome J. Form. Log. 35, 471–495 (1994)
Chagrov, A., Zakharyaschev, N.: Modal Logic. Oxford University Press (1997)
Corsi, G.: Weak logics with strict implication. Math. Log. Q. 33, 389–406 (1987)
Došen, K.: Modal translation in K and D. Diamond and Defaults, pp. 103–127 (1993)
Dragalin, A.: Mathmatical Intuitionism: Introduction to Proof Theory. American Mathematics Society (1988)
Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. Math. Log. 51, 71–92 (2012)
Gödel, K.: Eine interpretation des intuitionistischen Aussagenkalküls. Ergebnisse Eines Mathematischen Kolloquiums 4, 39–40 (1933)
Hughes, G., Cresswell, M.: A New Introduction to Modal Logic. Routledge, London (1996)
Ishigaki, R., Kashima, R.: Sequent calculi for some strict implication logics. Log. J. IGPL 16(2), 155–174 (2008)
Ishii, K., Kashima, R., Kikuchi, K.: Sequent calculi for Visser’s propositional logics. Notre Dame J. Form. Log. 42(1), 1–22 (2001)
Kikuchi, K.: Relationships between basic propositional calculus and substructural logics. Bull. Sect. Log. 30(1), 15–20 (2001)
Kikuchi, K., Sasaki, K.: A cut-free Gentzen formulation of basic propositional calculus. J. Log. Lang. Inf. 12, 213–225 (2003)
Kleene, S.C.: Introduction to Metamathematics. North-Holland Public Co. (1952)
Lewis, C.I.: Implication and the algebra of logic. Mind 21, 522–531 (1912)
Lewis, C.I.: A new algebra of strict implications and some consequents. J. Philos. Psychol. Sci. Methods 10, 428–438 (1913)
Ma, M., Sano, K.: On extensions of basic propositional logic. In: Proceedings of the 13th Asian Logic Conference, pp. 170–200 (2015)
Mckinsey, J.C.C., Tarski, A.: Some theorems about the sentential calculi of Lewis and Heyting. J. Symbol. Log. 13, 1–15 (1948)
Mints, G.: The Gödel-Tarski translations of intuitionistic propositional formulas. Correct Reason. 487–491 (2012)
Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34, 507–544 (2005)
Negri, S.: Proof analysis in non-classical logics. Logic Colloquium’ 05,ASL Lecture Notes in Logic, vol. 28, pp. 107–128 (2008)
Negri, S.: The intensional side of algebraic-topological representation theorems. Submitted
Negri, S., Von Plato, J.: Structural Proof Theory. Cambridge University Press (2001)
Negri, S., Von Plato, J.: Proof Analysis. Cambridge University Press (2011)
Restall, G.: Subintuitionistic logics. Notre Dome J. Form. Log. 35, 116–129 (1994)
Ruitenburg, W.: Constructive logic and the paradoxes. Modern Log. 1, 271–301 (1991)
Sano, K., Ma, M.: Alternative semantics for Visser’s propositional logics. In: Logic, Language, and Computation, volume 8984 of Lecture Notes in Computer Science, pp. 257–275 (2015)
Suzuki, Y., Ono, H.: Hilbert-style proof system for BPL. Technical Report IS-RR-97-0040F, Japan Advanced Institute of Science and Technology (1997)
Suzuki, Y., Wolter, F., Zakharyaschev, M.: Speaking about transitive frames in propositional languages. J. Log. Lang. Inf. 7, 317–339 (1998)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press (2000)
Visser, A.: A propositional logic with explicit fixed points. Studia Logica 40, 155–175 (1998)
Acknowledgments
We would like to thank an anonymous reviewer for his/her invaluable comments. We also would like to thank Sara Negri for her sharing her draft [23] on a similar topic to our paper. We are grateful to Ryo Kashima for setting opportunities for the first author to give presentations on this topic at Tokyo Institute of Technology for giving helpful suggestions to us. The first author wishes to thank her supervisor Kengo Okamoto for a regular weekly discussion. The authors have presented material related to this paper at several occasions. We would like to thank the audiences of these events, including 2014 annual meetings of the Japan Association for Philosophy of Science in Japan, Trends in Logic XIII in Poland, the Second Taiwan Philosophical Logic Colloquium (TPLC 2014) in Taiwan, and the 49th MLG meeting at Kaga, Japan. The first author’s visit to Taiwan for attending TPLC 2014 was supported by the grant from Tokyo Metropolitan University for graduate students. The work of the second author was partially supported by JSPS Core-to-Core Program (A. Advanced Research Networks) and JSPS KAKENHI, Grant-in-Aid for Young Scientists (B) 24700146 and 15K21025.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Yamasaki, S., Sano, K. (2016). Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics. In: Yang, SM., Deng, DM., Lin, H. (eds) Structural Analysis of Non-Classical Logics. Logic in Asia: Studia Logica Library. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48357-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-48357-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48356-5
Online ISBN: 978-3-662-48357-2
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)