Definition:Classes of WFFs/Plain WFF

From ProofWiki
Jump to: navigation, search


A plain WFF of predicate logic is a WFF with no parameters.

Thus $WFF \left({\mathcal P, \mathcal F, \varnothing}\right)$ is the set of all plain WFFs with relation symbols from $\mathcal P$ and function symbols from $\mathcal F$.

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