Abstract
We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof, which has been formalised in the Coq proof assistant, easily extends to the case of the absurdity connective using Kripke models with exploding nodes.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Veldman, W.: An intuitionistic completeness theorem for intuitionistic predicate logic. J. Symb. Log. 41(1), 159–166 (1976)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction I and II. Studies in Logic and the Foundations of Mathematics, vol. 121, 123. North-Holland, Amsterdam (1988)
Coquand, C.: From Semantics to Rules: A Machine Assisted Analysis. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, pp. 91–105. Springer, Heidelberg (1994)
Berger, U., Eberl, M., Schwichtenberg, H.: Normalisation by Evaluation. In: Möller, B., Tucker, J.V. (eds.) NADA 1997. LNCS, vol. 1546, pp. 117–137. Springer, Heidelberg (1998)
Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theor. Comput. Sci. 281(1-2), 471–498 (2002)
Danos, V., Joinet, J.B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication. In: Advances in Linear Logic, vol. 222, pp. 211–224. Cambridge University Press, Cambridge (1995)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Herbelin, H.: A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)
Herbelin, H.: Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, Université Paris 7 (January 1995)
Kripke, S.: A Completeness Theorem in Modal Logic. J. Symb. Log. 24(1), 1–14 (1959)
Kripke, S.: Semantical considerations on modal and intuitionistic logic. Acta Philos. Fennica 16, 83–94 (1963)
Kreisel, G.: On Weak Completeness of Intuitionistic Predicate Logic. J. Symb. Log. 27(2), 139–158 (1962)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development (Coq’Art: The Calculus of Inductive Constructions). EATCS Texts in Theoretical Computer Science, vol. XXV. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herbelin, H., Lee, G. (2009). Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2009. Lecture Notes in Computer Science(), vol 5514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02261-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-02261-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02260-9
Online ISBN: 978-3-642-02261-6
eBook Packages: Computer ScienceComputer Science (R0)