\begin{definition}[Definition:Classes of WFFs]
Let $\LL_1$ denote the language of predicate logic.
The set of all WFFs of $\LL_1$ formed with relation symbols from $\PP$ and function symbols from $\FF$ can be denoted $\map {WFF} {\PP, \FF}$.
If so desired, the parameters can also be emphasized by writing $\map {WFF} {\PP, \FF\ ,KK}$ instead.
To specify $\PP$, one speaks of '''WFFs with relation symbols from $\PP$'''.
To specify $\FF$, one speaks of '''WFFs with function symbols from $\FF$'''.
To specify $\KK$, one speaks of '''WFFs with parameters from $\KK$'''.
Of course, combinations of these are possible.
Several classes of WFFs are often considered and have special names.
\end{definition}