\begin{definition}[Definition:Classes of WFFs/Plain WFF]
A '''plain WFF''' of predicate logic is a WFF with no parameters.
Thus $\map {WFF} {\PP, \FF, \O}$ is the set of all '''plain WFFs''' with relation symbols from $\PP$ and function symbols from $\FF$.
{{ExtractTheorem|However immediate, this goes on a proof page}}
It is immediate that a '''plain WFF''' is a WFF with parameters from $\KK$ for ''all'' choices of $\KK$.
\end{definition}