9
$\begingroup$

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.

Improve this question
$\endgroup$
21
  • $\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 ♦
    Commented Dec 20, 2018 at 23:46
  • $\begingroup$ For how large a fragment of logic can you prove the reflection principle for IZF? $\endgroup$
    – Andrej Bauer
    Commented Dec 21, 2018 at 7:08
  • 2
    $\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
    Commented Dec 24, 2018 at 15:25
  • 1
    $\begingroup$ @aws Lubarsky provides an answer of the independence of Reflection over $\mathbf{CZF}$ in his article Independence Results around Constructive ZF. $\endgroup$
    – Hanul Jeon
    Commented Feb 19, 2019 at 4:15
  • 1
    $\begingroup$ @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). $\endgroup$
    – aws
    Commented Feb 19, 2019 at 9:21

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .