Forcing in intuitionistic systems without power-set

DOI10.2307/2273459zbMath0595.03056OpenAlexW2058730231MaRDI QIDQ3726114

Robin J. Grayson

Publication date: 1983

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2273459

zbMATH Keywords

exponentspower setscomplete setcovering familyconstructive higher order logic and set theoryinterpretation of the first order language

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55) Other aspects of forcing and Boolean-valued models (03E40)

Related Items

Growth functions on Fuchsian groups and the Euler characteristic, A constructive and functorial embedding of locally compact metric spaces into locales, A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra, Intuitive counterexamples for constructive fallacies, Derived rules for predicative set theory: an application of sheaves, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, The associated sheaf functor theorem in algebraic set theory, On some peculiar aspects of the constructive theory of point-free spaces, Forcing in Proof Theory, Wellfounded trees in categories, Growth series for the group \(\langle x,y\mid x^{-1}yx=y^ l\rangle\), Heyting-valued interpretations for constructive set theory

Cites Work

• Set theoretic foundations for constructive analysis
• Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
• An interpretation of intuitionistic analysis
• The consistency of classical set theory relative to a set theory with intu1tionistic logic