Results on forcing extensions for models of CZF

Question

I regard the research on models of ZFC, forcing extensions and related subjects as pretty promising with respect to coping with the incompleteness of ZFC. However, for certain applications I find constructive theories like CZF more applicable.

So, my question is on comparable results on models of CZF or maybe other constructive set theories. Maybe someone knows of some papers where models of constructive theories were researched with a glimpse on cross-model implications. Or papers where existing results on models for ZFC were researched with respect to their applicability on a constructive theory.

I guess there will be some differences, for starters because models of ZFC are supposed to define everything as either true or false, while non-constructive theories are not supposed to have a law of excluded middle.

My apologies for not being able to put this into a more definitive question, but I'm really having problems finding something where to start here, despite having already researched for applicable papers.

Answer 1

You may be interested in Gambino's article on forcing over CZF:

Nicola Gambino. Heyting-valued interpretations for Constructive Set Theory. Annals of Pure and Applied Logic 137, 2006, 164-188.

In this article, Gambino developed the theory of forcing over $\mathsf{CZF}^-$, namely, Constructive ZF without Subset collection. (Subset collection is a predicative substitute for the axiom of Power set, in a nutshell.) As an application of his model, Gambino showed that $\mathsf{CZF}^-$ and $\mathsf{CZF}^-$ with the excluded middle for bounded formulas ($\mathsf{\Delta_0}\text{-}\mathsf{LEM}$) are equiconsistent.

Rathjen and Swan made a futher application of Gambino's Heyting-valued models in

Michael Rathjen and Andrew Swan, Lifschitz Realizability as a Topological Construction. arXiv preprint. arXiv:1806.10047.

They showed in this article that $\mathsf{LLPO}_n$ is consistent with some non-classical axioms like $\mathsf{CT}_!$. ($\mathsf{CT}_!$ is the assertion that every functional relation over $\omega$ has a computable choice function. For the definition of $\mathsf{LLPO}_n$, see Chapter 8 of Diener's Constructive Reverse Mathematics.) Furthermore, they also showed that $\mathsf{CZF+MP+LLPO}_n$ has some existence property.

If we do not restrict our attention to $\mathsf{CZF}$, then articles by Lubarsky (e.g. this article) provide examples of applications of forcing over $\mathsf{IZF}$.