On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem. (English) Zbl 07450676

Summary: The Komori-Kashima problem, that asks whether (or not) the implicational intermediate logics axiomatizable by formulas minimal in classical logic are only intuitionistic logic and classical logic, has stood for over a decade. In this paper, we give a counter-example to this problem. Additionally, we also give some open problems derived from this result.


03-XX Mathematical logic and foundations
Full Text: DOI


[1] Barendregt, H., W. Dekkers, and R. Statman, Lambda Calculus with Types, Cambridge University Press, 2013. · Zbl 1347.03001
[2] Dummett, Michael, A Propositional Calculus with Denumerable Matrix, The Journal of Symbolic Logic, 24, 2, 97-106 (1959) · Zbl 0089.24307
[3] Dyckhoff, Roy, Contraction-Free Sequent Calculi for Intuitionistic Logic, The Journal of Symbolic Logic, 57, 3, 795-807 (1992) · Zbl 0761.03004
[4] Hirai, Y., Personal Communication (Aug 9 2018), 2018.
[5] Jankov, VA, On the extension of the intuitionist propositional calculus to the classical calculus, and the minimal calculus to the intuitionist calculus, Mathematics of the USSR-Izvestiya, 2, 1, 205-208 (1968) · Zbl 0191.28602
[6] Jankov, V. A., The Calculus of the Weak “Law of Excluded Middle”, Mathematics of the USSR-Izvestiya 2(5):997-1004, 1968. · Zbl 0187.26306
[7] Kashima, R., On non-generality of axioms of intermediate propositional logics (in Japanese), available at http://www.is.titech.ac.jp/
[8] Kashima, R., Problems on Axiomatization of Intermediate Propositional Logics, in the 39th MLG meeting in 2005, pp.59-62 (available at http://www.st.nanzan-u.ac.jp/info/sasaki/2005mlg/59-62.pdf), 2005.
[9] Komori, Y., BCK algebras and lambda calculus, in Proceedings of 10th Symposium on Semigroups, Sakado 1986, 1987, pp. 5-11.
[10] Komori, Y., A problem on logics axiomatized with formulas minimal in classical logic, and more (in Japanese), in the Mathematical Society of Japan Autumn Meeting 2005 (available at http://komoriyuichi.web.fc2.com/gakkai/05-09/kyokusyou/gakkai.pdf), 2005.
[11] Komori, Y., Independent Axiom Systems of Minimal formulas for Classical Logic, in The 39th MLG meeting in 2005 (available at http://www.st.nanzan-u.ac.jp/info/sasaki/2005mlg/56-58.pdf), 2005, pp. 56-58.
[12] Komori, Y., Propositional logics revisited - deployments from misunderstanding and mistakes (in Japanese), in The Mathematical Society of Japan Autumn Meeting 2007 (available at doi:10.11429/emath1996.2007.autumn-meeting1_82), The Mathematical Society of Japan, 2007,pp. 82-94.
[13] Nakamura, Y., Coq Files for “On the Axiomatization of Implicational Intermediate Logics with Formulas Minimal in Classical Logic: A Counter-Example to the Komori-Kashima Problem”, available at https://bitbucket.org/yoshikinakamura/komori-kashima-coq, 2020.
[14] The Coq Development Team, The Coq Proof Assistant, Version 8.10.0, available at doi:10.5281/zenodo.3476303, 2019.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.