Abstract
We give an alternative proof of (a slightly strong form of) the completeness of two second order propositional intuitionistic logics with respect to Kripke models. One is the logic having the full comprehension axiom, and the other has the constant domain axiom in addition. We also show that, if the language does not contain disjunction as a primitive symbols, then the constant domain axiom is not needed for the completeness with respect to constant domain models. To show the completeness, we use the technique of nested sequent calculi.
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
Fitting, M. (2014). Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1), 41–61.
Gabbay, D. M. (1974). On 2nd order intuitionistic propositional calculus with full comprehension. Archive for Mathematical Logic, 16, 177–186.
Kashima, R. (2016). Completeness of second order propositional intuitionistic logics. Technical report, Tokyo Institute of Technology, from http://www.is.titech.ac.jp/~kashima/pub/C284.pdf.
Okada, M. (2002). A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science, 281, 471–498.
Prawitz, D. (1970). Some results for intuitionistic logic with second order quantification rules. In A. Kino, J. Myhill, & R. E. Vesley (Eds.), Intuitionism and Proof Theory, Proceedings of the Summer Conference at Buffalo N.Y. 1968 (pp. 259–269): North-Holland. chapter 17.
Sobolev, S. K. (1977). The intuitionistic propositional calculus with quantifiers. Mathematical Notes, 22, 528–532. (English version of Mat. Zametki 22:69–76 (1977)).
Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the curry-howard isomorphism. 0: Elsevier.
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
Kashima, R. (2017). On Second Order Propositional Intuitionistic Logics. 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_9
Download citation
DOI: https://doi.org/10.1007/978-981-10-6355-8_9
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)