CZF is touted as the predicative and constructive variant of ZF. This is because CZF avoids the fully impredicative axioms of powerset and full separation and alternatively because CZF has an interpretation in an extension of Martin Löf’s type theory, which is predicative. One typically says the definition of an object is impredicative if it contains quantification over a collection of which the object is a member. Now just as there are different versions of constructivism there are different versions of predicativism. But in many monographs that discuss predicativism among the already mentioned impredicative principles another hallmark definition is deemed impredicative: the least upper bound of a set. This is because for one to define the least upper bound $s$ of a subset $S$ of $X$ one must quantify over the set of upper bounds of $S$ which of course contains $s$.
Work with in CZF by both Azcel and Rathejen uses the notion of a least upper bound (or sup or join) frequently so this begs the question: are impredicative definitions allowed in CZF (and other predicative theories?) Is it impredicative constructions that are cause for concern to someone seeking to develop a predicative theory?
Edit: It’s been established that predicativity is not a well-defined notion. I am looking for insight from people that do predicative mathematics.
Best Answer
As Zhen Lin said, whether impredicativity is considered (potentially) problematic generally comes down to description vs. construction.
It doesn't really make sense to worry about something merely because we have some impredicative description of it. You might be able to come up with all sorts of impredicative properties satisfied by or even uniquely characterizing things you have (somehow) separately established the existence of. 0 is the least natural number. 1 is the least odd natural number. Tea is the most tea-like beverage.
In the context of CZF, this is presumably the sort of situation, "least upper bound," is. It is a description of a property that an object may or may not have. If you use CZF to give a predicative construction of a value, and demonstrate that it has the property of being a least upper bound of something, then it's irrelevant that the description of "least upper bound" is impredicative. The description wasn't used to exhibit the value.
The reason that people are wary of things like power sets is that they are one of the rules for building new things. Given a set $X$, we simply assert that $\mathcal{P} X$ also exists, rather than predicatively 'building up' to something that satisfies its description. And the obvious reason for this is that in general it's not clear that you can build it 'from below.' It's not clear that some 'big' set you haven't thought of yet won't allow you to pick out a new subset of $ℕ$, say, that hadn't been previously identifiable.
A simplified example of this would be imagining a very finite analogue of CZF. You only consider quantifiers over particular finite sets. Then, even most constructivists would say that ideally, you can just exhaustively check the truth of any proposition, and the collection of propositions is adequately modeled by a $2$ element set. The power set of a $4$ element set is then a $16$ element set, and so on. You can build up to the power set of any other finite set eventually, just by combining finite sets in predicative ways.
However, once we can quantify over infinitely many things, we can no longer even ideally hope to decide propositions by exhaustive checking. It's not clear that we can decide them at all, and that is the sort of standard constructivists want to assert $P ∨ ¬P$. There is no hope to reach the power set by defining more finite sets, because the infinite sets give rise to "sub-finite" sets that are not finite, but also not infinite. The power set of a finite set must contain all of these sets that are not reachable just by building up enough finite sets.
We can relax from our very limited system where no proposition can contain an unbounded quantifier to a more accurate finite analogue of CZF. Now propositions can have unbounded quantifiers, but there are no power sets assumed and no unbounded separation. Now, I believe we still cannot show that any non-finite sets exist. We can only separate by propositions that are exhausively checkable, so separation will always produce a finite set. So, in some sense, this theory agrees with the limited (, more obviously predicative) one about which sets there are. However, because propositions in general can contain unbounded quantifiers, what it means to be a power set is different. In particular, they wouldn't be finite sets, and presumably couldn't be shown to exist except by axiom.
I think CZF vs. IZF is probably a similar scenario, although I'm not an expert. You could possibly imagine a restriction of CZF with only bounded quantifiers, and it would agree with CZF about what sets exist. CZF would just be able to describe some additional properties that those sets have. The first thing is the sort of predicativity that people actually worry about, because it is the source of paradoxes.