Forcing in intuitionistic systems without power-set
- 1 September 1983
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 48 (3) , 670-682
- https://doi.org/10.2307/2273459
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.Keywords
This publication has 7 references indexed in Scilit:
- Heyting-valued models for intuitionistic set theoryPublished by Springer Nature ,1979
- Identity and existence in intuitionistic logicPublished by Springer Nature ,1979
- Sheaves and logicPublished by Springer Nature ,1979
- Sheaf models for analysisPublished by Springer Nature ,1979
- An interpretation of intuitionistic analysisAnnals of Mathematical Logic, 1978
- Principles of continuous choice and continuity of functions in formal systems for constructive mathematicsAnnals of Mathematical Logic, 1977
- Set Theoretic Foundations for Constructive AnalysisAnnals of Mathematics, 1977