On the complexity of propositional quantification in intuitionistic logic

Journal of Symbolic Logic 62 (2):529-544 (1997)
  Copy   BIBTEX


We define a propositionally quantified intuitionistic logic Hπ + by a natural extension of Kripke's semantics for propositional intutionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π +, S4π +, S4.2π +, K4π +, Tπ +, Kπ + and Bπ +, studied by Fine



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

84 (#196,199)

6 months
14 (#170,850)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Philip Kremer
University of Toronto at Scarborough

References found in this work

Propositional quantifiers in modal logic.Kit Fine - 1970 - Theoria 36 (3):336-346.
Completeness in the Theory of Types.Leon Henkin - 1950 - Journal of Symbolic Logic 16 (1):72-73.
Semantical Investigations in Heyting's Intuitionistic Logic.Dov M. Gabbay - 1986 - Journal of Symbolic Logic 51 (3):824-824.
Propositional Quantifiers in Modal Logic.Kit Fine - 1970 - Journal of Symbolic Logic 38 (2):329-329.

View all 7 references / Add more references