Forcing in intuitionistic systems without power-set
Robin J. Grayson · Journal of Symbolic Logic · 1983
Abstract It is shown how to define forcing semantics within metatheories not containing the power-set construction, in particular, how to construct exponents assuming only (a slightly strengthened form of) exponents in the metatheory. Some straightforward applications (consistency and independence results, and derived rules) are obtained for such systems.