Forcing in intuitionistic systems without power-set

DOI10.2307/2273459MaRDI QIDQ3726114zbMATH OpenOpenAlexFDO

Authors 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

complete setconstructive higher order logic and set theorycovering familyexponentsinterpretation of the first order languagepower sets

Mathematics Subject Classification ID

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

Recommendations

• Independence results around constructive ZF
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• On power set in explicit mathematics
• Formal topologies on the set of first-order formulae

Cites work

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

Cited in

(21)

• Growth functions on Fuchsian groups and the Euler characteristic
• 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
• On some peculiar aspects of the constructive theory of point-free spaces
• A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra
• Derived rules for predicative set theory: an application of sheaves
• Forcing in Proof Theory
• Intuitive counterexamples for constructive fallacies
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively
• A constructive and functorial embedding of locally compact metric spaces into locales
• The associated sheaf functor theorem in algebraic set theory

This page was built for publication: Forcing in intuitionistic systems without power-set

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3726114)