Fine and Kripke extended S5, S4, S4.2 and such to produce propositionally quantified systems , , : given a Kripke frame, the quantifiers range over all the sets of possible worlds. is decidable and, as Fine and Kripke showed, many of the other systems are recursively isomorphic to second-order logic. In the present paper I consider the propositionally quantified system that arises from the topological semantics for S4, rather than from the Kripke semantics. The topological system, which I dub , (...) is strictly weaker than its Kripkean counterpart. I prove here that second-order arithmetic can be recursively embedded in . In the course of the investigation, I also sketch a proof of Fine's and Kripke's results that the Kripkean system is recursively isomorphic to second-order logic. (shrink)

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.