# Definition:Classes of WFFs

This page has been identified as a candidate for refactoring of advanced complexity.In particular: Get rid of $\KK$. In the current setup, constant symbols don't really get separate attention, and I definitely want to stop calling them "parameters"Until this has been finished, please leave
`{{Refactor}}` in the code.
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}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Definition

Let $\LL_1$ denote the language of predicate logic.

The set of all WFFs of $\LL_1$ formed with relation symbols from $\PP$ and function symbols from $\FF$ can be denoted $\map {WFF} {\PP, \FF}$.

If so desired, the parameters can also be emphasized by writing $\map {WFF} {\PP, \FF\ ,KK}$ instead.

To specify $\PP$, one speaks of **WFFs with relation symbols from $\PP$**.

To specify $\FF$, one speaks of **WFFs with function symbols from $\FF$**.

To specify $\KK$, one speaks of **WFFs with parameters from $\KK$**.

Of course, combinations of these are possible.

Several classes of WFFs are often considered and have special names.

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

This page or section has statements made on it that ought to be extracted and proved in a Theorem page.In particular: However immediate, this goes on a proof pageYou can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by creating any appropriate Theorem pages that may be needed.To discuss this page in more detail, feel free to use the talk page. |

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

### Sentence

A WFF is said to be a **sentence** if and only if it contains no free variables.

To denote particular classes of **sentences**, $\map {SENT} {\PP, \FF, \KK}$ and analogues may be used, similar to the notation for classes of WFFs.

### Plain Sentence

A WFF is said to be a **plain sentence** if and only if it is both plain and a sentence.

That is, if and only if it contains free variables nor parameters.

Thus, **plain sentences** are those WFFs which are in $\map {SENT} {\PP, \FF, \O}$.

## Sources

- 1996: H. Jerome Keisler and Joel Robbin:
*Mathematical Logic and Computability*: $\S 2.3$