Abstract
Albert Visser introduced a subintuitionistic logic called Basic Propositional Logic (\(\mathbf {BPL}\)) by dropping the requirement of reflexivity from Kripke semantics for intuitionistic logic, and he showed that \(\mathbf {BPL}\) can be embedded into modal logic \(\mathbf {K4}\) by a semantic method. This paper provides a contraction-free non-labelled sequent calculus for \(\mathbf {BPL}\) and shows that the calculus enjoys the admissibility of cut. Moreover, we establish a proof-theoretic embedding from \(\mathbf {BPL}\) into \(\mathbf {K4}\) via a Gödel–McKinsey–Tarski translation.
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
References
Aghaei, M., & Ardeshir, M. (2001). Gentzen-style axiomatizations for some conservative extentions of basic propositional logic. Studia Logica, 68(2), 263–285.
Alizadeh, M., & Ardeshir, M. (2006). Amalgamation property for the class of basic algebras and some of its natural subclasses. Archive for Mathematical Logic, 45, 913–930.
Ardeshir, M. (1995). Aspects of Basic Logic. Ph.D thesis, Marquette University.
Ardeshir, M., & Ruitenburg, W. (2001). Basic propositional calculus II, interpolation. Archive for Mathematical Logic, 40, 349–364.
Chagrov, A., & Zakharyaschev, M. (1997). Modal logic. Oxford: Oxford University Press.
Corsi, G. (1987). Weak logics with strict implication. Mathematical Logic Quarterly, 33, 389–406.
Craig, W. (1957). Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic, 22(3), 250–268.
Dyckhoff, R., & Negri, S. (2012). Proof analysis in intermediate logics. Archive for Mathematical Logic, 51, 71–92.
Goble, L. (1974). Gentzen systems for modal logics. Notre Dame Journal of Formal Logic, 15, 455–461.
Gödel, K. (1933). Eine interpretation des intuitionistischen Aussagenkalküls. Ergebnisse Eines Mathematischen Kolloquiums, 4, 39–40.
Ishigaki, R., & Kashima, R. (2008). Sequent calculi for some strict implication logics. Logic Journal of the IGPL, 16(2), 155–174.
Ishii, K., Kashima, R., & Kikuchi, K. (2001). Sequent calculi for Visser’s propositional logics. Notre Dame Journal of Formal Logic, 42(1), 1–22.
Kikuchi, K. (2001). Relationships between basic propositional calculus and substructural logics. Bulletin of the Section of Logic, 30(1), 15–20.
Ma, M.,& Sano, K. (2015). Extensions of Basic Propositional Logic. In X. Zhao, X. Feng, B. Kim, & L. Yu (Eds.), Proceedings of the 13th Asian Logic Conference, 13th Asian Logic Conference, Guangzhou, China, 16–20 September 2013, World Scientific (pp. 170–200).
Maehara, S. (1954). Eine Darstellung der intuitionistischen Logik in der klassischen. Nagoya Mathematical Journal, 7, 45–64.
McKinsey, J. C. C., & Tarski, A. (1948). Some theorems about the sentential calculi of Lewis and Heyting. Journal of Symbolic Logic, 13, 1–15.
Mints, G. (2012). The Gödel-Tarski Translations of Intuitionistic Propositional Formulas. In E. Erdem, J. Lee, Y. Lierler, & D. Pearce (Eds.), Correct Reasoning. Lecture Notes in Computer Science (Vol. 7265, pp. 487–491). Berlin, Heidelberg: Springer.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge University Press.
Prawitz, D., & Malmnäs, P.-E. (1968). A survey of some connections between classical, intuitionistic and minimal logic. Studies in Logic and the Foundations of Mathematics, 50, 215–229.
Restall, G. (1994). Subintuitionistic logics. Notre Dame Journal of Formal Logic, 35, 116–129.
Ruitenburg, W. (1991). Constructive logic and the paradoxes. Modern Logic, 1(4), 271–301.
Ruitenburg, W. (1993). Basic logic and fregean set theory. Drik van Dalen Festschrift, Quaestiones Infinitae, 5, 121–142.
Sambin, G., & Valentini, S. (1982). The modal logic of provability. The sequential approach. Journal of Philosophical Logic, 11(3), 311–342.
Suzuki, Y.,& Ono, H. (1997). Hilbert-style proof system for BPL. Technical Report IS-RR-97-0040F, Japan Advanced Institute of Science and Technology.
Suzuki, Y., Wolter, F., & Zakharyaschev, M. (1998). Speaking about transitive frames in propositional languages. Journal of Logic, Language and Information, 7(3), 317–339.
Troelstra, A.S.,& Schwichtenberg, H. (2000). Basic proof theory, 2nd edn. Cambridge: Cambridge University Press.
Visser, A. (1981). A propositional logic with explicit fixed points. Studia Logica, 40(2), 155–175.
Yamasaki, S., & Sano, K. (2016). Constructive embedding from extensions of logics of strict implication into modal logics. In S. M. Yang, D. M. Deng, & H. Lin (Eds.), Structural analysis of non-classical logics, Logic in Asia: Studia Logica Library (pp. 223–251). Berlin, Heidelberg: Springer.
Acknowledgements
We would like to thank an anonymous reviewer for his/her invaluable comments and suggestions. In particular we owe the reviewer for the simple notation used in (Step 2) and (Step 3) of the case (v) in the proof of Theorem 1. We are grateful to Ryo Kashima for setting opportunities for the first author to give the presentation on this topic at Tokyo Institute of Technology. We would like to thank the audiences of the events where the content of this paper is presented, including the 50th MLG meeting at Kyoto, Japan, The Joint Conference of The Third Asian Workshop on Philosophical Logic (AWPL 2016) and The Third Taiwan Philosophical Logic Colloquium (TPLC 2016) in Taiwan. The first author’s visit to Taiwan was supported by the grant from travel awards for students and young researchers of AWPL-TPLC 2016. The work of the first author was supported by JSPS KAKENHI Grant Number JP 15J07255. The work of the second author was partially supported by JSPS KAKENHI Grant-in-Aid for Young Scientists (B) Grant Number 15K21025 and JSPS Core-to-Core Program (A. Advanced Research Networks).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Yamasaki, S., Sano, K. (2017). Proof-Theoretic Embedding from Visser’s Basic Propositional Logic to Modal Logic K4 via Non-labelled Sequent Calculi. In: Yang, SM., Lee, K., Ono, H. (eds) Philosophical Logic: Current Trends in Asia. Logic in Asia: Studia Logica Library. Springer, Singapore. https://doi.org/10.1007/978-981-10-6355-8_12
Download citation
DOI: https://doi.org/10.1007/978-981-10-6355-8_12
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-6354-1
Online ISBN: 978-981-10-6355-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)