Definition:Classes of WFFs

From ProofWiki
Jump to: navigation, search

Definition

Let $\mathcal L_1$ denote the language of predicate logic.


The set of all WFFs of $\mathcal L_1$ formed with relation symbols from $\mathcal P$ and function symbols from $\mathcal F$ can be denoted $WFF \left({\mathcal P, \mathcal F}\right)$.

If so desired, the parameters can also be emphasized by writing $WFF \left({\mathcal P, \mathcal F, \mathcal K}\right)$ instead.


To specify $\mathcal P$, one speaks of WFFs with relation symbols from $\mathcal P$.

To specify $\mathcal F$, one speaks of WFFs with function symbols from $\mathcal F$.

To specify $\mathcal K$, one speaks of WFFs with parameters from $\mathcal K$.

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


Sentence

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

To denote particular classes of sentences, $SENT \left({\mathcal P, \mathcal F, \mathcal K}\right)$ and analogues may be used, similar to the notation for classes of WFFs.


Plain Sentence

A WFF is said to be a plain sentence iff it is both plain and a sentence.

That is, if it contains free variables nor parameters.


Thus, plain sentences are those WFFs which are in $SENT \left({\mathcal P, \mathcal F, \varnothing}\right)$.


Sources