Timeline for Reflection principle for intuitionistic Zermelo–Fraenkel?
Current License: CC BY-SA 4.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 19, 2019 at 9:21 | comment | added | aws | @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). | |
| Feb 19, 2019 at 4:15 | comment | added | Hanul Jeon | @aws Lubarsky provides an answer of the independence of Reflection over $\mathbf{CZF}$ in his article Independence Results around Constructive ZF. | |
| Jan 10, 2019 at 21:36 | comment | added | Ingo Blechschmidt | @aws: The reflection principle seems to be equivalent to $\mathbf{RRS}_2$, the following strengthening of $\mathbf{RRS}$: Let $X$ and $R \subseteq X \times X \times X$ be classes. Assume $\forall x \in X. \forall x' \in X. \exists y \in X. \langle x,x',y \rangle \in R$. Let $A \subseteq X$ be a set. Then there is a set $B$ such that $A \subseteq B \subseteq X$ and such that $\forall x \in B. \forall x' \in B. \exists y \in B. \langle x,x',y \rangle \in R$. | |
| Jan 10, 2019 at 16:03 | comment | added | Ingo Blechschmidt | @aws: I now noticed a problem even with the case of existential quantifiers. The proof of Lemma 3.4 only works in the case of a single free variable. I'm trying to fix this by encoding multiple values by tuples, but the naive way doesn't seem to work because we cannot ensure that the partial universe $M$ is closed under pairs. | |
| Jan 9, 2019 at 20:30 | comment | added | Ingo Blechschmidt | @aws: Anyway, no matter how not earth-shattering the whole story is, I do think that it deserves to be written up and hence started doing so. You should definitely be coauthor! Please feel free to contact me at [email protected]. | |
| Jan 9, 2019 at 20:29 | comment | added | Ingo Blechschmidt | @aws: That's a neat trick! I too think that universal quantifiers can be treated with it. By the way, using the equivalent $\mathbf{MDC}$ (Palmgren's multivalued dependent choice) instead of $\mathbf{RRS}$ seems to make the proofs (very slightly) easier, at least for my taste. Regarding $\mathbf{CZF}$: I believe that by now we have used unbounded separation far too often, right? :-) That is, independence of $\mathbf{RRS}$ from $\mathbf{CZF}$ will not immediately help us to settle independence over $\mathbf{IZF}$. | |
| Jan 9, 2019 at 19:46 | comment | added | aws | There's a generalisation of the trick for existential formulas: Let $\Omega$ be the power set of $1$. For a formula $\phi(x)$, define $X := \{ p \in \Omega | \exists x \, p \Leftrightarrow \phi(x) \}$. Then by collection there is $C$ such that for all $x$ there is $x' \in C$ such that $\phi(x) \Leftrightarrow \phi(x')$. I think universal quantifiers might be possible using that idea. The situation with $\mathbf{CZF}$ is a bit different to how I expected - I need to think about it some more. | |
| Jan 8, 2019 at 23:51 | comment | added | Ingo Blechschmidt | @aws: Thank you for the pointer to $\mathbf{RRS}$! I see that the reflection principle implies $\mathbf{RRS}$. I also see the converse, but only for formulas which don't contain the universal quantifier. Probably you meant to restrict to this class of formulas, right? Yes; I'd also be very much interested in the situation for $\mathbf{CZF}$. | |
| Jan 8, 2019 at 21:33 | comment | added | aws | By the way, are you interested in the same problem for $\mathbf{CZF}$? I think for $\mathbf{CZF}$ it should be much easier to prove independence - I have a rough idea in mind for that. | |
| Jan 8, 2019 at 21:29 | comment | added | aws | While I was looking into it I was reminded of Aczel's Relation Reflection Scheme. I think in fact reflection should be equivalent to $\mathbf{RRS}$ over $\mathbf{IZF}$. (But I don't know how to show that $\mathbf{RRS}$ is independent.) | |
| Jan 8, 2019 at 21:26 | comment | added | aws | Nice! I think I can guess how that works. The problem is I also don't know how to separate $\mathbf{RDC}$ from $\mathbf{DC}$. | |
| Jan 8, 2019 at 20:46 | comment | added | Ingo Blechschmidt | (And upon further reflection, I see that the argument can be simplified to use the reflection principle only once.) | |
| Jan 8, 2019 at 20:27 | comment | added | Ingo Blechschmidt | @aws: Yes, that's it, thank you for the reference! And now I think we have a proof that the reflection principle does not hold for $\mathbf{IZF}$: If it would, then by applying the reflection principle twice, in a mostly but not entirely straightforward way (I could provide details if interested), we could show that that IZF proves that DC implies RDC. Which it presumably doesn't, even though, not being particularly familiar with IZF, I don't personally know a model in which DC holds but RDC doesn't. | |
| Jan 4, 2019 at 15:43 | comment | added | aws | It's enough to have relativised dependent choice, I think (in section 10.2 of Aczel and Rathjen). | |
| Jan 4, 2019 at 14:58 | comment | added | Ingo Blechschmidt | @aws: Let me add a correction to my previous comment. I stated that dependent choice would be enough. That's not true, because it's not clear that there is a set of suitable sets we could apply choice ot. We'd need some form of choice for iterative non-deterministic constructions of sets. | |
| Jan 2, 2019 at 15:43 | comment | added | Ingo Blechschmidt | @aws: I see. We'd need definability, or, failing that, unique existence (among all other candidate sets $C'$ with some property) in order to avoid having to appeal to the axiom of dependent choice. Very interesting! I'll think about this some more. | |
| Dec 24, 2018 at 15:27 | comment | added | aws | 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}$. | |
| Dec 24, 2018 at 15:25 | comment | added | aws | @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. | |
| Dec 21, 2018 at 14:06 | comment | added | Ingo Blechschmidt | @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. | |
| Dec 21, 2018 at 7:08 | comment | added | Andrej Bauer | For how large a fragment of logic can you prove the reflection principle for IZF? | |
| Dec 20, 2018 at 23:46 | comment | added | David Roberts♦ | 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?) | |
| Dec 20, 2018 at 23:45 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
added 82 characters in body; edited tags
|
| Dec 20, 2018 at 23:39 | history | migrated | from math.stackexchange.com (revisions) | ||
| Dec 15, 2018 at 21:00 | history | asked | Ingo Blechschmidt | CC BY-SA 4.0 |