Example 2

The relation $x \neq x$ is not collectivizing in $x$; in other words, (not $\operatorname{Coll}_x(x \neq x)$) is a theorem. Let us argue by contradiction and suppose that $x \neq x$ is collectivizing. Let $a$ be an auxiliary constant, distinct from $x$ and the constants of the theory, with the introductory axiom

Then the relation

is true by C30 (Chapter I, §4, no. 3). The method of disjunction of cases (Chapter I, §3, no. 3) shows first that the relation $a \neq a$ is true, and then that the relation $a \in a$ is true, which is absurd.

C49. Let $R$ be a relation and $x$ a letter. If $R$ is collectivizing in $x$, the relation $(\forall x)((x \in y) \Longleftrightarrow R)$, where $y$ is a letter distinct from $x$ which does not appear in $R$, is functional in $y$.

This follows immediately from C48.

Very often in what follows we shall have at our disposal a theorem of the form $\operatorname{Coll}_xR$. To represent the term

which does not depend on the choice of the letter $y$ (distinct from $x$ and not appearing in $R$), we shall introduce a functional symbol $\mathscr{E}_x(R)$; the corresponding term does not contain $x$. This term is denoted by “the set of all $x$ such that $R$”. By definition (Chapter I, §4, no. 1) the relation

is identical with $\mathrm{Coll}_x R$; consequently the relation $R$ is equivalent to

C50. Let $R$, $S$ be two relations and let $x$ be a letter. If $R$ and $S$ are collectivizing in $x$, the relation $(\forall x)(R \Rightarrow S)$ is equivalent to

and the relation $(\forall x)(R \Leftrightarrow S)$ is equivalent to $\mathscr{E}_x(R) = \mathscr{E}_x(S)$.

This follows immediately from the preceding remark and from Definition 1 and axiom A1.