Can we define an object in a predicative and also in an impredicative way?

Question

I wonder if there are some objects that one could define in a predicative way and also in an impredicative way. I mean, two defenitions for the same object.

Thanks.

Edit: although I did get an answer for my question from Derek Elkins. I am editing for future googlers because I recieved some comments about the topic not being cleared. Examples for objects:

• R = {S | S ∉ S} (Russell's paradox) - Impredicative, because R is a set (in the naive sense) and S is ranging over all possible sets
• Let x be the smallest element in S” - Impredicative, because x is a member of S
• Let π be the ratio between the circumference and diameter of a circle” - predicative

I wanted to find a predicative defenition and an impredicative defenition for the same object.

Answer 1

As briefly covered on the nLab for Grothendieck toposes, it turns out you can't prove that a Grothendieck topos (by one definition) is cocomplete in a finitist, predicative foundation. Given either W-types, including natural numbers, or impredicativity you can. The core problem is the notion of transitive closure. In a finitist, predicative mathematics, you can't define the transitive closure of an arbitrary relation. In more traditional mathematics, there are two equivalent ways of defining the transitive closure of a relation.

The first is to say the transitive closure of a relation, $R$, is the smallest transitive relation that contains $R$. The definition doesn't require any infinite sets to exist, but it does require that you can quantify over "all transitive relations containing $R$" which is impredicative in general.

The second is to say the transitive closure of a relation, $R \subseteq X\times X$, is the relation $R^*$ where $R^*(x,y)$ if and only if there exists a list of elements of $X$, $(x_i)_{i=0}^n$ such that $x = x_0$ and $x_n = y$ and $R(x_{i-1},x_i)$ for $i \in \{1,\dots, n\}$. This definition is predicative but not finitist since it's based on lists.

The nLab page on pretoposes gives a brief but decent break-down of what kinds of math you get as you assume different structure. (Of course, you don't need to start at a pretopos.) This provides one way of interpreting what "finitist" or "predicative" mathematics is.