Definition:Classes of WFFs/Plain WFF

From ProofWiki
Jump to navigation Jump to search


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$.

It is immediate that a plain WFF is a WFF with parameters from $\KK$ for all choices of $\KK$.