# Impredicative Definitions (CZF)

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.

• The definition of least upper bound quantifies over all upper bounds. The construction is a different matter. For example, I think you will not find any constructivist who denies that the least upper bound of a set of two natural numbers exists. Commented Jan 6, 2022 at 11:39
• Certainly. I am just trying to understand what line can not be crossed before one admits a theory impredicative. Does one allow impredicative definitions but avoid impredicative axioms/theorems/proofs. Commented Jan 6, 2022 at 15:46

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.

• This answer is very deep and I don’t think I was able to fully appreciate it at the time it was given. Commented Mar 30, 2022 at 18:49
• Can we discuss the union axiom with respect to your analogues? It’s not at all difficult to see how a union is built up for finite sets. You simply look at the elements of each family member and include it in a new collection. Can we extend this notion back to full CZF? Surely we can or otherwise the union axiom would have been under suspicion. Commented Mar 30, 2022 at 18:59

According to What is predicativism? the kind of circularity that should not be forbidden occurs when one picks out an element of an existing collection. Expanding on this a bit: the definition of an element is forbidden (predicativly) if it is definable ONLY in terms of collections to which it belongs.

This is AN answer. But where does this leave the definition of least upper bound. If you are given an arbitrary non empty subset $$S \subseteq X$$ it seems like quantifying over the upper bounds is the same as picking out an element of an existing collection and should not be forbidden. But this seems in contrast with the claim by many predicative papers that least upper bound is a hallmark impredicative definition.

• Do you have an example of a paper where the authors have a problem with the notion of the least upper bound of a set? Commented Jan 9, 2022 at 20:04
• Your question talks about certain impredicative things being "forbidden." What is an example of a paper that says that least upper bounds should be forbidden for being impredicative? In general there is no universal agreement about exactly which things are (im)predicative, or which impredicativity is actually cause for concern. So it'd be helpful to see an example of someone concerned about least upper bounds to be able to elaborate on why that particular author was wary about them. Commented Jan 10, 2022 at 4:01
• Defining something does not make it exist. Commented Jan 11, 2022 at 0:57
• Sure. You can talk about anything you like. Impredicativity is not a thoughtcrime. Commented Jan 11, 2022 at 1:27
• I don’t understand your confusion. Just because some concrete thing viewed one way has an impredicative characterisation doesn’t mean it must be rejected in predicative mathematics – it could have a predicative characterisation viewed another way. The same mutatis mutandis for constructive mathematics more generally. (Try looking up the fact that the so-called axiom of choice is a theorem of Martin-Löf type theory!) Commented Jan 11, 2022 at 2:24