“Large” Dependent Choice in IZF

115 Views Asked by At

The scheme of “large dependent choice” (LDC) consists of statements of the form

Suppose $\forall x \exists y P(x,y)$. Then for all $z$, there is some infinite sequence $\{s_i\}_{i \in \mathbb{N}}$ such that $s_0 = z$ and $\forall i \in \mathbb{N} P(s_i, s_{i + 1})$.

The ordinary version of dependent choice (DC) can be phrased as a single axiom, which is (the universal closure of) the following:

Suppose $P \subseteq A^2$. And further suppose $\forall x \in A \exists y \in A ((x, y) \in P)$. Then for all $z \in A$, there exists a sequence $\{s_i\}_{i \in \mathbb{N}}$ such that $s_0 = z$ and $\forall i \in \mathbb{N} (s_i, s_{i + 1}) \in P$

In ZF, every instance of LDC follows from DC. This can be proved using Scott’s trick.

Is the same true in IZF (with collection)?

1

There are 1 best solutions below

0
On BEST ANSWER

Your large dependence choice is known as Relativized Dependent Choice ($\mathsf{RDC}$). It is known by Aczel that $\mathsf{CZF}$ proves $\mathsf{RDC}$ is equivalent to the combination of $\mathsf{DC}$ and Relation Reflection Scheme ($\mathsf{RRS}$). You can find Aczel's proof from

Aczel, Peter (2008). The Relation Reflection Scheme. Mathematical Logic Quarterly 54 (1):5-11.

As far as I know, it is open whether $\mathsf{IZF+DC}$ proves $\mathsf{RRS}$ or not. However, it is known by Swan and Blechschmidt (on their unpublished note) that $\mathsf{RRS_2}$, a strengthening of $\mathsf{RRS}$, is equivalent to the reflection principle over $\mathsf{IZF}$. (Note that, it is also open whether $\mathsf{IZF}$ proves the reflection principle.)