Definition:Classes of WFFs/Plain WFF
Jump to navigation
Jump to search
This page has been identified as a candidate for refactoring. In particular:
However immediate, this goes on a proof page
Definition
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$.
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 $\KK$ for all choices of $\KK$.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$