# 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.

-

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?

-
Thanks for your informative answer. Maybe self-referential is a better term in this context than circular. BTW I am not sure that Ramsey's example is impredicative. Informally, Jane is not freshly constructed, she's existing already. What we define is a predicate $tallestInRoom$ (that happens to hold of Jane). And the predicate is not defined in a self-referential way. This is quite different with the usual impredicative definition of eg. the natural numbers in set theory, where you bring about the set only by the impredicative definition. – Martin Berger May 30 '13 at 8:07
Another question: would you happen to have a (natural) example of a definition in ZF(C) where it's unclear if it's impredicative or not? – Martin Berger May 30 '13 at 8:08
Ah, but that's exactly the issue (as Gödel pointed out): should we think of e.g. a set of numbers as "brought about" by its definition or as existing there already, waiting to be picked out by us [like Jane]. Should we be constructivists or realists about e.g. sets of numbers? If you are a constructivist about $X$s, you'll care about avoiding impredicativity about $X$s; if you are a realist about $X$s then you won't. – Peter Smith May 30 '13 at 8:18
So the "Jane" example is an example of an unworrying impredicative way of picking something out, as we are naively realistic about Jane [unless we have been corrupted by philosophy!] But it is technically impredicative. – Peter Smith May 30 '13 at 8:22
I think the real reason people (used to) worry about impredicativity isn't to do with realism or otherwise, is was more because there was a lingering fear that impredicative definitions would eventually turn out to be contradictory. Time has assuaged this worry. That said, I don't particularly care about such issues. I'm interested in the syntactic shape of (im)predicative definitions. I have an intuitive idea why e.g. the impredicative definition of the natural numbers in ZF is unproblematic, and it's a syntactic criterion. – Martin Berger May 30 '13 at 8:44