There have been many debates about impredicative definitions in set theory, trying to judge whether they are good or bad.
I'm not sure I understand them, because first-order logic theories can be formulated without any definitions at all. To me, a definition is adding a symbol to the logical signature, along with an axiom for it. For example, ZFC set theory can be formulated with a signature consisting of a single binary relation $\in$, representing set membership, and the usual axioms about it.
Of course, with this minimalistic signature the formulas will be much too long to handle for a human. But still, it is theoretically possible and a computer could check such formulas and the formal proofs about them.
To make formulas shorter, I can introduce a new nullary constant $\emptyset$ in the signature, along with the axiom $\forall a, \, a \notin \emptyset$. Then I claim I have defined the empty set and can start using it in formulas. And conversely, if I want to go back to low-level formulas, I can replace every occurrence of $\emptyset$ by $\exists e, (\forall a, a\notin e), \dots$ Likewise for an impredicative definition, such as the greatest lower bound of a subset of the reals. The new symbol is a unary operation $Glb$ and its axiom is $$ \forall A\subset\mathbb{R}, \; Glb(A) \in \{ y \in \mathbb{R} \mid y \leq A\} \land \forall x \in \{ y \in \mathbb{R} \mid y \leq A\}, x \leq Glb(A) $$
So how can there be debates about impredicative definitions, that I can completely remove if I wish?
And what exactly is called impredicative in the examples above? The new logical symbols? The axioms that mention them? What if I state 2 axioms concerning the greatest lower bound :
- $ \forall A\subset\mathbb{R}, \;Glb(A) \in \{ y \in \mathbb{R} \mid y \leq A\} $
- $ \forall A\subset\mathbb{R}, \;\forall x \in \{ y \in \mathbb{R} \mid y \leq A\}, x \leq Glb(A) $
Does any of them, separately, define $Glb(A)$? In the most general case, an impredicativity seems a collection of axioms, with respect to a collection of symbols. But in what form exactly? Does impredicativity only concern set theory, or does it exist in for example first-order Peano arithmetic?