Definition:Classes of WFFs/Plain WFF
Definition
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$.
However immediate, this goes on a proof page
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
It is immediate that a plain WFF is a WFF with parameters from $\mathcal K$ for all choices of $\mathcal K$.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
