{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T23:48:15Z","timestamp":1771544895914,"version":"3.50.1"},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6128,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1997,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We define a propositionally quantified intuitionistic logic <jats:bold>H<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+ by a natural extension of Kripke's semantics for propositional intuitionistic logic. We then show that <jats:bold>H<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+ is recursively isomorphic to full second order classical logic. <jats:bold>H<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+ is the intuitionistic analogue of the modal systems <jats:bold>S5<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+, <jats:bold>S4<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+, <jats:bold>S4.2<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+, <jats:bold>K4<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+, <jats:bold>T<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+, <jats:bold>K<jats:italic>\u03c0<\/jats:italic><\/jats:bold>+ and <jats:bold>B<jats:italic>\u03c0<\/jats:italic>+<\/jats:bold>, studied by Fine.<\/jats:p>","DOI":"10.2307\/2275545","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T23:01:20Z","timestamp":1146956480000},"page":"529-544","source":"Crossref","is-referenced-by-count":29,"title":["On the complexity of propositional quantification in intuitionistic logic"],"prefix":"10.1017","volume":"62","author":[{"given":"Philip","family":"Kremer","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200016340_ref005","first-page":"355","author":"Kaplan","year":"1970","journal-title":"S5 with quantifiable propositional variables"},{"key":"S0022481200016340_ref008","first-page":"92","volume-title":"Formal systems and recursive functions: Proceedings of the eighth logic colloquium","author":"Kripke","year":"1963"},{"key":"S0022481200016340_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2977-2"},{"key":"S0022481200016340_ref001","first-page":"336","volume-title":"Theoria","author":"Fine","year":"1970"},{"key":"S0022481200016340_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71260-6"},{"key":"S0022481200016340_ref012","first-page":"58","volume-title":"Logic, methodology and the philosophy of science, proceeding of the 1964 international congress","author":"Rabin","year":"1965"},{"key":"S0022481200016340_ref002","first-page":"177","volume-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforsch","author":"Gabbay","year":"1974"},{"key":"S0022481200016340_ref004","first-page":"81","author":"Henkin","year":"1950","journal-title":"Completeness in the theory of types"},{"key":"S0022481200016340_ref006","first-page":"9","volume-title":"Reports on Mathematical Logic","author":"Kreisel","year":"1981"},{"key":"S0022481200016340_ref007","first-page":"334","author":"Kremer","year":"1993","journal-title":"Quantifying over propositions in relevance logic: Non-axiomatisability of \u2200p and \u2203p"},{"key":"S0022481200016340_ref009","first-page":"705","author":"L\u00f6b","year":"1976","journal-title":"Embedding first order predicate logic in fragments of intuitionistic logic"},{"key":"S0022481200016340_ref011","first-page":"33","author":"Pitts","year":"1992","journal-title":"On an interpretation of second order quantification in first order intuitionistic propositional logic"},{"key":"S0022481200016340_ref013","first-page":"155","volume-title":"Annals of Pure and Applied Logic","author":"Scedrov","year":"1984"},{"key":"S0022481200016340_ref014","first-page":"69","volume-title":"Akademiya Nauk Soyuza SSR. Matematicheskie Zamietki","author":"Sobolev","year":"1977"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200016340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T20:55:49Z","timestamp":1557608149000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200016340\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,6]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,6]]}},"alternative-id":["S0022481200016340"],"URL":"https:\/\/doi.org\/10.2307\/2275545","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,6]]}}}