# Reflection principle for intuitionistic Zermelo–Fraenkel?

The well-known reflection principle for classical Zermelo–Fraenkel states:

For any formula $$\varphi(x_1,\ldots,x_n)$$ of the language of ZFC with free variables $$x_1,\ldots,x_n$$, ZFC proves $$\forall M_0. \exists M \supseteq M_0. \forall x_1,\ldots,x_n \in M. (\varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^M(x_1,\ldots,x_n)),$$ where $$\varphi^M$$ is the $$M$$-relativization of $$\varphi$$.

Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.

Surely this has been studied before, but I wasn't able to track down a reference.

Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.

• I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?) – David Roberts Dec 20 '18 at 23:46
• For how large a fragment of logic can you prove the reflection principle for IZF? – Andrej Bauer Dec 21 '18 at 7:08
• @IngoBlechschmidt you can prove that using full separation and collection. Define $X := \{ x \in \{0\} | (\exists y)y \in C \}$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' \cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(\exists y)\phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely. – aws Dec 24 '18 at 15:25
• @aws Lubarsky provides an answer of the independence of Reflection over $\mathbf{CZF}$ in his article Independence Results around Constructive ZF. – Hanul Jeon Feb 19 '19 at 4:15
• @HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $\mathbf{CZF}$ with powerset and $\mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset). – aws Feb 19 '19 at 9:21