Page:Russell, Whitehead - Principia Mathematica, vol. I, 1910.djvu/104

which, again, is equivalent to

$\scriptstyle {(\exists \chi ):\phi x.\equiv _{x}.\chi !x:\psi x.\equiv _{x}.\chi !x}$,

which, in virtue of the axiom of reducibility, is equivalent to

$\scriptstyle {\phi x.\equiv _{x}.\psi x}$.

Thus our definition of the use of $\scriptstyle {{\hat {z}}(\phi z)}$ is such as to satisfy the conditions (2) and (3) which we laid down for classes, i.e. we have

$\scriptstyle {\vdash :.{\hat {z}}(\phi z)={\hat {z}}(\psi z).\equiv :\phi x.\equiv _{x}.\psi x}$.

Before considering classes of classes, it will be well to define membership of a class, i.e. to define the symbol "$\scriptstyle {x\in {\hat {z}}(\phi z)}$," which may be read "$\scriptstyle {x}$ is a member of the class determined by $\scriptstyle {\phi {\hat {z}}}$." Since this is a function of the form $\scriptstyle {f\{{\hat {z}}(\phi z)\}}$, it must be derived, by means of our general definition of such functions, from the corresponding function $\scriptstyle {f\{\phi !{\hat {z}}\}}$. We therefore put

$\scriptstyle {x\in \psi !{\hat {z}}.=.\psi !x\quad {\text{Df.}}}$

This definition is only needed in order to give a meaning to "$\scriptstyle {x\in {\hat {z}}(\phi z)}$"; the meaning it gives is, in virtue of the definition of $\scriptstyle {f\{{\hat {z}}(\phi z)\}}$,

$\scriptstyle {(\exists \psi ):\phi y.\equiv _{y}.\psi !y:\psi !x}$.

It thus appears that "$\scriptstyle {x\in {\hat {z}}(\phi z)}$" implies $\scriptstyle {\phi x}$, since it implies $\scriptstyle {\psi !x}$, and $\scriptstyle {\psi !x}$ is equivalent to $\scriptstyle {\phi x}$; also, in virtue of the axiom of reducibility, $\scriptstyle {\phi x}$ implies "$\scriptstyle {x\in {\hat {z}}(\phi z)}$," since there is a predicative function $\scriptstyle {\psi }$ formally equivalent to $\scriptstyle {\phi }$, and $\scriptstyle {x}$ must satisfy $\scriptstyle {\psi }$, since $\scriptstyle {x}$ (ex hypothesi) satisfies $\scriptstyle {\phi }$. Thus in virtue of the axiom of reducibility we have

$\scriptstyle {\vdash :x\in {\hat {z}}(\phi z).\equiv .\phi x}$,

i.e. $\scriptstyle {x}$ is a member of the class $\scriptstyle {{\hat {z}}(\phi z)}$ when, and only when, $\scriptstyle {x}$ satisfies the function $\scriptstyle {\phi }$ which defines the class. We have next to consider how to interpret a class of classes. As we have defined $\scriptstyle {f\{{\hat {z}}(\phi z)\}}$, we shall naturally regard a class of classes as consisting of those values of $\scriptstyle {{\hat {z}}(\phi z)}$ which satisfy $\scriptstyle {f\{{\hat {z}}(\phi z)\}}$. Let us write $\scriptstyle {\alpha }$ for $\scriptstyle {{\hat {z}}(\phi z)}$; then we may write $\scriptstyle {{\hat {\alpha }}(f\alpha )}$ for the class of values of $\scriptstyle {\alpha }$ which satisfy $\scriptstyle {f\alpha }$^[1]. We shall apply the same definition, and put

$\scriptstyle {F\{{\hat {\alpha }}(f\alpha )\}.=:(\exists g):f\beta .\equiv _{\beta }.g!\beta :F\{g!{\hat {\alpha }}\}\quad {\text{Df}}}$,

where "$\scriptstyle {\beta }$" stands for any expression of the form $\scriptstyle {{\hat {z}}(\psi !z)}$. Let us take "$\scriptstyle {\gamma \in {\hat {\alpha }}(f\alpha )}$" as an instance of $\scriptstyle {F\{{\hat {\alpha }}(f\alpha )\}}$. Then

$\scriptstyle {\vdash :.\gamma \in {\hat {\alpha }}(f\alpha ).\equiv :(\exists g):f\beta .\equiv _{\beta }.g!\beta :\gamma \in g!{\hat {\alpha }}}$.

Just as we put

$\scriptstyle {x\in \psi !{\hat {z}}.=.\psi !x\quad {\text{Df}}}$,

so we put

$\scriptstyle {\gamma \in g!{\hat {\alpha }}.=.g!\gamma \quad {\text{Df.}}}$

Thus we find

$\scriptstyle {\vdash :.\gamma \in {\hat {\alpha }}(f\alpha ).\equiv :(\exists g):f\beta .\equiv _{\beta }.g!\beta :g!\gamma }$.

1. The use of a single letter, such as $\scriptstyle {\alpha }$ or $\scriptstyle {\beta }$, to represent a variable class, will be further explained shortly.