The axiom schema of predicative separation says that, for a set X and a predicate F containing only bounded quantifiers, there exists a set whose members are exactly those members of X which satisfy F. As I understand it, a bounded quantifier is a quantifier of the form (∀x∈X) or (∃x∈X), where X is a set. If I’m interpreting this correctly, then, for a function f from X to Y, where X and Y are both sets, {y∈Y:(∃x∈X)(f(x)=y)} is a set.
Here’s my problem. Let denote the set {0,1}. Let α:ℕ→ be an arbitrary binary sequence. ℕ is clearly a set, as is , so, by the axiom schema of predicative separation, {x∈:(∃n∈ℕ)(α(n)=x)} or Im(α) is a set, in particular, a subset of . Because is finite, its power-set P()={∅,{0},{1},} is constructible and finite, so we can exhaustively check which values in P() Im(α) can take. By definition of a function, we know that since ℕ is inhabited, Im(α) is inhabited, so it can’t equal the empty set. Assume that Im(α)={0}; then (∀n∈ℕ)(α(n)=0). Assume that Im(α)={1} or Im(α)=; then (∃n∈ℕ)(α(n)=1). Because α is arbitrary, this implies the limited principle of omniscience, that (∀α:ℕ→)((∀n∈ℕ)(α(n)=0)∨(∃n∈ℕ)(α(n)=1)), which constructive logicians reject.
I'm confident I must have misunderstood something, because it doesn't feel quite right that the axiom schema of predicative separation alone should prove something nonconstructive. I think my logic is fine, so I'm guessing my mistake is in my interpretation of either the axiom schema of predicative separation or bounded quantifiers; or maybe I haven't adequately defined in which system of constructive set theory I've been working. I really don't know, and any help would be greatly appreciated.
Usually, constructive mathematics will reject the assertion that $P(\{ 0, 1 \}) = \{ \emptyset, \{ 0 \}, \{ 1 \}, \{ 0, 1 \} \}$, considering this to be essentially a product of two instances of the law of excluded middle.
For a slightly smaller example, let $\phi$ be any predicate with bounded quantifiers and with no free variables. Then $S := \{ x \in \{ 0 \} \mid \phi \}$ is in $P(\{ 0 \})$. However, if we assert that $P(\{ 0 \}) = \{ \emptyset, \{ 0 \} \}$, then $S = \emptyset$ is equivalent to $\lnot \phi$, and $S = \{ 0 \}$ is equivalent to $\phi$. So, in this way, the assertion that $P(\{ 0 \}) = \{ \emptyset, \{ 0 \} \}$ is equivalent to claiming that the law of excluded middle holds on all predicates with bounded quantifiers - at least in the presence of the axiom schema of predicative separation.
That said, we often are interested in when a certain subset of $X$ is decidable, i.e. when membership in that subset is a decidable proposition for each $x \in X$. In the language of topos theory, for example, with a subobject classifier $\Omega$ representing a set of possible truth values, the full power set of $X$ would correspond to functions $X \to \Omega$ whereas the set of decidable subsets of $X$ would correspond to functions $X \to \{ T, F \}$; and we do not necessarily have $\Omega = \{ T, F \}$.