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.


migrated from math.stackexchange.com Dec 20 '18 at 23:39

This question came from our site for people studying math at any level and professionals in related fields.

  • $\begingroup$ 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?) $\endgroup$ – David Roberts Dec 20 '18 at 23:46
  • $\begingroup$ For how large a fragment of logic can you prove the reflection principle for IZF? $\endgroup$ – Andrej Bauer Dec 21 '18 at 7:08
  • $\begingroup$ @Andrej: Currently only for the empty fragment, that is, not at all; but if a version of Scott's trick could be salvaged (given a class $C$, we need a subset $C'$ with the property that $C'$ is inhabited if $C$ is), then for the fragment not containing the universal quantifier. $\endgroup$ – Ingo Blechschmidt Dec 21 '18 at 14:06
  • 1
    $\begingroup$ @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. $\endgroup$ – aws Dec 24 '18 at 15:25
  • $\begingroup$ When I first saw this question I thought I had a proof of reflection in $\mathbf{IZF}$ using that kind of trick. Now I think it's more likely that it's not provable in $\mathbf{IZF}$. $\endgroup$ – aws Dec 24 '18 at 15:27

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.