Is (im)predicativity decidable The distinction between predicative and impredicative definitions is
important in mathematics. As first approximation, impredicativity
means circularity. Let me give you an example of an impredicative
definition.
Let $V$ be a vector-space over a field $K$, and $S \subseteq V$ a set
of vectors. The ${span}$ of $S$ is the intersection of all
sub-vector-spaces $V'$ of $V$ that also contain $S$.
$$
\operatorname{span}(S) = \bigcap \{V'\ |\ S \subseteq V', V'\ \text{is a sub-vector-space of}\ V\}
$$
In a set theory like ZF(C), this definition is impredicative
because $\operatorname{span}(S)$ is itself a member of $\{V'\ |\ S \subseteq V',\
\text{is a sub-vector-space of}\ V\}$.  In some sense this definition
is circular. In this particular case, we can easily get around this
impredicativity, for example by defining
$$
\operatorname{span}(S) = \{\Sigma _{i=1}^{n} k_i.v_i\ |\ n \geq 0, k_i \in K, v_i \in S\}
$$
but it's not always that easy. For example in ZF(C) the natural numbers are often defined as follows.
$$
  \mathbb{N} = \bigcap \{S \ |\ S\ \text{is an inductive set}\}
$$
where $S$ set is inductive if it contains $0$ and is closed
under successor. Clearly, $\mathbb{N}$ is itself inductive.
Such circularities are not considered problematic in classical
mathematics, in the sense that no contradictions have ever been
derived from such impredicative definitions. Nevertheless,
impredicate definitions don't always sit well with constructive
mathematics. This leads to my question: is it always easy to see if a
definition is (im)predicative? More precisely:
Is it decidable if a formula $F$ is predicative in a theory $T$?
I'm most interested in the case where the theory $T$ is some set theory.
Note that I have not formally defined (im)predicativity. Such a
definition itself appears to be difficult, but I would be happy to
hear about answers to my question for any of the extant formal
or informal notions of (im)predicativity.
 A: 1] The usual characterization of an impredicative definition is that it defines some object (property, relation, function, etc.) by means of a quantification over some domain which, if the definition succeeds, contains that object (property, relation, function, etc.). Here quantifications will be taken to include Russellian definite descriptions, as when we define an object as the unique object such that ...
In the context of a formalized theory with typed variables, we typically implement a ban on impredicative definitions by banning definitions of things of type $t$ via formulas that involve quantifiers of type $t$. Thus, predicative second-order arithmetic is characterised by only allowing instances of the comprehension schema defining a numerical property [or set of numbers] to contain first-order quantifiers over numbers (and not second-order quantifiers over properties [sets of numbers]). And in such a context it is readily decidable by inspection whether a formula is predicative and can feature in the comprehension scheme or other kind of definition. 
2] But, as the OP hints, it can be interesting to ask when an impredicative definition has a co-extensive predicative counterpart. There's surely not usually going to be a decidable routine to determine that even within a fixed formalized theory (if only because we can't usually effectively determine co-extensionality).
3] As a footnote, pace Russell, it isn't particularly helpful to think of impredicativity as a species of circularity. To use Ramsey's example, if I pick out Jane as the tallest woman in the room, that's impredicative (I pick her out by a quantification over a totality including her); but in what sense is that circular?
