Yes, it is worth the effort. A predicative version of an impredicative construction is typically more explicit and informative than the impredicative one. For example, consider the construction of a subgroup $\langle S \rangle$ of a group $G$ generated by the set $S$:
- impredicative: $\langle S \rangle$ is the intersection of all subgroups of $G$ which contain $S$.
- predicative: $\langle S \rangle$ consists of all finite combinations of elements of $S$ and their inverses, i.e., a typical elements is $x_1 x_2 \cdots x_n$ where $x_i \in S \cup S^{-1}$.
This can be quite useful if you want to compute with groups (i.e., with a computer), as you will definitely prefer the second description, which tells you how exactly the elements of the subgroup can be represented.
Many examples of impredicative constructions are special cases of the following theorem.
Theorem (Knaster and Tarski): A monotone map on a complete lattice has a least fixed-point above every point.
To take two of your examples:
Subgroup generated by a set: the complete lattice is the powerset $P(G)$ of the group $G$ in question, and the map $f : P(G) \to P(G)$ takes $S \subseteq G$ to $f(S) = S \cup S^{-1} \cup S \cdot S$.
$\sigma$-algebra generated by a family of subsets: exercise.
There are two standard ways of proving the Knaster-Tarski theorem, one impredicative and one predicative. These exemplify the two general approaches of getting to desired objects "impredicatively from above" and "predicatively from below".
The impredicative proof goes as follows: call a point $x$ a prefixed point if $f(x) \leq x$. Consider the set $S$ of all prefixed points above a given point $y$ (which is not empty as it contains the top of the lattice). The least fixed-point above $y$ is the infimum $x = \inf S$ (exercise).
The predicative proof goes as follows: iterate $f$ starting with a given point $y$ to construct an increasing sequence $$y, f(y), f^2(y), \ldots, f^\omega(y), \ldots, f^\alpha(y), \ldots$$ where we have to iterate through ordinals until we're blue in the face. The iteration stops eventually, and that's the least fixed-point above $y$.
Of course, in such generality the predicative proof is hardly better than the impredicative one because we replaced one non-description with another. But in particular cases we might know something about $f$. For example, we might know that it preserves suprema of countable chains, as we do in the example of a subgroup generated by a set, in which case the iteration stops at $\omega$.
Your third example, namely the connected component of a point, can be dealt with also, but I am not sure it's any better than the impredicative construction:
- Connected components: the connected component of a point is a maximal connected subset containing it. You are probably thinking of the construction that says "just take the union of all connected subsets that contain the point". We could instead try the following: define $x \sim y$ to mean that for all continuous $f : X \to 2$, $f(x) = f(y)$. The connected components of $X$ are the equivalence classes of $\sim$. Therefore the connected component of a point is just its equivalence class. This is not entirely satisfactory as it replaces one bad description with another. Can we be more explicit? What if we have a nice basis for the space?
Sometime you have to reformulate the whole subject to get away from builtin impredicativity (and it is still worth doing because it gives computational meaning to theorems which are quite non-computational in the impredicative setting):
- Closure/interior of a set: under classical formulation of topology you can sometimes get away with predicative construction, for example if you can reduce your construction to manipulation of a countable topological basis, e.g. the interior of $S \subseteq \mathbb{R}$ is the union of all open intervals with rational endpoints that are contained in $S$. There are general formulations of topology, such as formal topology and Abstract Stone Duality, which avoid impredicative constructions altogether.
Lastly, you mention Dedekind completeness of reals. I am not sure this is impredicative. The supremum of a non-empty bounded family of left-sided Dedekind cuts is simply their union. What is impredicative about taking the union of a family of cuts?
Adendum: Note that in the typical case it is the construction, i.e., an existence proof, which is predicative or impredicative, not the definition. For example, the group generated by a set is defined as the least subgroup containing the generators, which has nothing to to with predicativity/impredicativity.
P.S. You need a better MO username.
