Hi, I met several times the expressions "predicative definition" and "unpredicative definiton" in texts about logic. What these expressions do mean ? I precise I'm a french student, thanks for your help.
A definition of an object X is called impredicative if it quantifies over a collection Y to which X itself belongs (or at least could belong). The classic example is the set occurring in Russell's paradox, defined by "the members of X are all sets s that are not members of themselves". This quantifies over all sets, including X itself.
But impredicative definitions occur (without paradox) in ordinary mathematics also. For example, one might define a real number r as the supremum of a set A that might have r itself among its members. Unraveling the definition of "supremum" we would find quantification over A (and indeed quantification over the set of all real numbers).
Russell proposed to eliminate the settheoretic and logical paradoxes by eliminating impredicative definitions, and "Principia Mathematica" (by Russell and Whitehead) develops an elaborate mechanism for this. Unfortunately, too much of ordinary mathematics was unprovable in that system, so Russell and Whitehead found it necessary to add the socalled axiom of reducibility, whose principal effect is to counteract the predicativityenforcing mechanism and make impredicative mathematics available again.

$\begingroup$ The supremum and Russell's paradox seem classical examples. I wonder about the definition of the identity element in GroupTheory. It is an element e for which ex = xe = x for all x. Since in this definition there is a quantification over all elements x, including e itself, is it not also an example of an impredicative definition? In which case, is there some reason why this example would be less important, or at least less referred to, than the others? $\endgroup$ – Tommy R. Jensen Oct 20 '19 at 22:33

$\begingroup$ Another instance that I wonder about is when Nelson in his 1986 pamphlet "predicative Arithmetic" states that "the principle of induction" is impredicative. How can induction fall into the scope of having an impredicative definition, given that "induction" is not a mathematical object? $\endgroup$ – Tommy R. Jensen Oct 20 '19 at 22:41

$\begingroup$ @TommyR.Jensen The identity element of a group admits an alternative definition, as the only element satisfying xx=x, so one can avoid impredicativity there. As for induction, I don't claim to understand Nelson's work, but he might have been referring to the usual settheoretic definition of $\mathbb N$ as the intersection of all sets that contain $0$ and are closed under successor. That definition, which implies the induction principle, is impredicative because $\mathbb N$ itself is a set that contains $0$ and is closed under successor. $\endgroup$ – Andreas Blass Oct 21 '19 at 3:13

$\begingroup$ I would think that definition of $\mathbb{N}$ is not usual in settheories like ZF, since it seems to assume a set of all inductive sets, to allow defining their intersection. It sounds similarly bad as the "set of all sets". $\endgroup$ – Tommy R. Jensen Oct 22 '19 at 11:26

1$\begingroup$ @TommyR.Jensen In ZF, the axiom of infinity says there is an inductive set. Then one defines $\mathbb N$ as the intersection of all inductive subsets of an inductive set $A$, after proving that the resulting $\mathbb N$ is independent of the choice of $A$. $\endgroup$ – Andreas Blass Oct 22 '19 at 12:09
I don't think "predicative" has a generally accepted precise definition, though roughly speaking it refers to definitions of objects that only depend on previously constructed objects. For example, the axiom of replacement in set theory is impredicative because it constructs new sets, but the construction involves quantifying over all sets, including the one you are trying to construct. The FefermanSchutte ordinal is sometimes said to be the first impredicative ordinal (though I've never really understood why), in which case predicative mathematics consists roughly of theorems that only depend on transfinite induction up to smaller ordinals.

$\begingroup$ If my view of the axioms of ZF is that, whenever I am presented with some given structure, the axioms allow me to decide whether or not the structure is a model of ZF, and all that is needed is to verify or fail to verify them. Is it then not natural that it is hard for me to grasp the meaning of these terms? After all, it is how structures in math are first presented to students. Example: a textbook presents a composition table for $S_3$ and you are required to verify from the axioms that $S_3$ is a group. In particular, nothing seems "constructed". $\endgroup$ – Tommy R. Jensen Oct 29 '19 at 15:52