# Definition:Language of Predicate Logic/Formal Grammar

## Definition

Part of specifying the language of propositional logic is to provide its formal grammar.

The following rules of formation constitute a bottom-up grammar for the language of predicate logic $\mathcal L_1$.

The definition proceeds in two steps.

First, we will define terms, and then well-formed formulas.

### Terms

The terms of $\mathcal L_1$ are identified by the following bottom-up grammar:

 $(\mathbf T \ \textrm {VAR})$ $:$ Any variable of $\mathcal L_1$ is a term; $(\mathbf T \ \mathcal F_n)$ $:$ Given an $n$-ary function symbol $f \in \mathcal F_n$ and terms $\tau_1, \ldots, \tau_n$: $\map f {\tau_1, \ldots, \tau_n}$ is also a term.

### Well-Formed Formulas

The WFFs of $\mathcal L_1$ are defined by the following bottom-up grammar:

 $(\mathbf W ~ \mathcal P_n)$ $:$ If $t_1, \ldots, t_n$ are terms, and $p \in \mathcal P_n$ is an $n$-ary predicate symbol, then $p \left({t_1, t_2, \ldots, t_n}\right)$ is a WFF. $(\mathbf W ~ \neg)$ $:$ If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF. $(\mathbf W ~ \lor, \land, \Rightarrow, \Leftrightarrow)$ $:$ If $\mathbf A, \mathbf B$ are WFFs and $\circ$ is one of $\lor, \land, \mathord\implies, \mathord\iff$, then $\left({\mathbf A \circ \mathbf B}\right)$ is a WFF $(\mathbf W ~ \forall, \exists)$ $:$ If $\mathbf A$ is a WFF and $x$ is a variable, then $\left({\forall x: \mathbf A}\right)$ and $\left({\exists x: \mathbf A}\right)$ are WFFs.