Impredicativity in first order logic

Question

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?

Answer 1

First, let me describe the general situation in first-order logic: In order to eliminate, in the way you've described, a defined function symbol that you've added to a theory $T$, you need to know that the original $T$ (without the new symbol $F$) can prove the existence and uniqueness of what you intend to call $F(x)$. That is, if your definition of $F$ says that $F(x)$ is the thing $y$ that satisfies a certain formula $\phi(x,y)$, then $T$ needs to prove that, for each $x$, there is a unique such $y$. Intuitively, the point is just that your definition $\phi(x,y)$ needs to define a particular object $F(x)$, which it won't if you don't have $(\forall x)(\exists!y)\,\phi(x,y)$. Technically, you should look into the proof that definitions can be eliminated and see that it really uses the existence and uniqueness of the defined object.

Now, let me talk about set theory, say the standard ZFC axioms. They allow you to introduce lots of definitions, like the $\emptyset$ and the $Glb$ that you mentioned in the question, because these axioms are strong enough to prove the existence and uniqueness of these things. But they would not allow you to introduce, for example, a symbol $U$ for the universe with the "definition" that everything is a member of $U$; ZFC doesn't prove that such a $U$ exists (in fact, it proves that no such $U$ exists).

The issue of predicativity doesn't arise in ZFC because its axioms are strong enough to give you existence and uniqueness of lots of sets whose definitions are impredicative. Notice in particular that the axioms of separation and replacement allow arbitrary formulas, with no predicative restrictions on the domains of quantification.

But one could certainly design (and people have designed) alternative axiomatic systems that don't assume the existence of impredicatively defined sets. People working with such a system of axioms (still in first-order logic) would have to work harder when adding definitions. They'd need to make sure that their axioms ensure the existence and uniqueness of the things they want to define. And, if those things are sets, they might need to check predicativity in order to apply their axioms.