Understanding predicativity

The set of even numbers has a predicative definition: a number $n$ is even if and only if there is a number $k$ with $k = 2n$. That definition does not quantify over sets at all, just over numbers. More generally, a definition of a set of natural numbers which only quantifies over numbers, and not over sets, is usually seen as predicative.

The term "predicative", however, does not have a completely clear and formal definition. There are some mathematical systems that are often thought of as "predicative" and others that are usually thought of as "impredicative", but the dividing line is not clear. This is similar to the definition of "constructive" - there is no firm definition of what makes a mathematical system constructive.

So, rather than learning about predicativity/impredicativity from definitions, you have learn about it from examples. Like "beauty", "constructivism", and "elegance", the idea of "predicativity" is more suited for philosophy of mathematics (or "metamathematics" in the broader sense) than for formal mathematics. However, as is common in the current approach, we can use formal results of mathematical logic to help clarify what is going on with the concept of predicativity, just as we can for constructivism. (Beauty and elegance are harder for us to explain formally with the current state of knowledge.)

As Professor Mummert has noted, the notion of a "predicative definition" is vague, although I would disagree that the same holds for "predicative mathematics". There are many complicated issues involved.

With respect to "definition", is it "obvious" that mathematics ought to be based upon "undefined primitives"? Russell and Whitehead made such a claim. You will find a detailed analysis with criticism of "Principia Mathematica" in the book $\underline{Definition}$ by Richard Robinson. Among the kinds of definitions one finds in non-foundational mathematics is "implicit definition". And, you will find that Professor Robinson does discuss them as legitimate forms of mathematical definition. When you think about the matter closely, you will realize that the "intensional definition" -- upon which Church introduced the lambda calculus -- is, in fact, a variation of implicit definition. The functions which Church introduced may be applied to themselves. Such functions are not representable in Zermelo-Fraenkel set theory because the axiom of foundation restricts that notion of set to being well-founded. Thus, the extension of a function in the sense of what Church did (that is, its representation as a set of ordered pairs) would have to appear as a domain element of the function. The axiom of foundation restricts against this infinite descending chains of membership relations.

Now, consider the definition,

$$\forall x \forall y ( x \subset y \leftrightarrow ( \forall z ( y \subset z \rightarrow x \subset z ) \wedge \exists z ( x \subset z \wedge \neg y \subset z ) ) )$$

I use this form of sentence for both the set theory and the arithmetic (interpreted as proper divisor) in which I am interested. The syntax is clearly circular. Is it an impredicative definition?

According to a monograph by Moschovakis, a sentence of this nature appears to be impredicative if one naively attributes it to be a second-order sentence but is, in fact, recursively constructive. And, indeed, you will find a sentence of this form used in $\underline{Set Theory}$ by Kunen in his discussion of forcing. By contrast, the full-blown transfinite recursion is presented by Jech in the first edition of his book $\underline{Set Theory}$.

When I say that "predicative mathematics" does not suffer from the same problem as "predicative definition", it is because it originates with Russell and Whitehead with the express purpose of avoiding the circularity which they believed responsible for the many early paradoxes in set theory. So, one understands sets, first and foremost, as collections of individuals which are not, themselves, a collection. Then, one may form additional sets from those individuals and those initial sets of individuals. The next "type" will be sets formed of "objects" previously obtained through "set formation". I apologize for finishing with all of these quotes. But, in natural language it gets complicated. In combination with the axioms of union and power set, the axiom of foundation provides for this structure.

This kind of distinction may be found in Aristotle. For Aristotle, individuals are primary substance. Notions such as "species" and "genus" are substances in the sense that what they categorize are individuals. But, Aristotle refers to them as secondary substances.

One of the interesting things one discovers when reading Aristotle is that his only admonition against circularity is that against trying to simultaneously attribute truth to deductive reasoning and inductive reasoning at the same time. In modern mathematics, this seems to be related to the Lyndon interpolation theorem. The proof of that theorem uses negation normal forms. The significance of this is the restricted second-order language presented by Flum and Ziegler in the early 1980's. Its formation rules are governed by negation normal forms while its semantics coincide with first-order semantics on trivial topologies and discrete topologies. It is clear that predicative mathematics will avoid invoking both the universal quantifier and the existential quantifier simultaneously. It emphasizes the existential quantifier as being semantically prior to the universal quantifier. But, without some accommodation to the logic, the syntactic definition of individuals (as opposed to relations) merely on the basis of "properties" puts one at risk of attributing truth to both the universal quantifier and the existential quantifier simultaneously.

This is what the distinction between "predicative definition" and "impredicative definition" is trying to restrict. But, it is not at all clear that a classification of definitions is the appropriate vehicle. What is at stake is the claim that "mathematics is extensional" and the interpretation of quantifiers as collections which are objects. The circularity of intensional definitions and recursive definitions does not seem to always lead to paradox.