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

The definition proceeds in two steps.

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

### Terms

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

 $(\mathbf T \ \textrm {VAR})$ $:$ Any variable of $\LL_1$ is a term; $(\mathbf T \ \FF_n)$ $:$ Given an $n$-ary function symbol $f \in \FF_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 $\LL_1$ are defined by the following bottom-up grammar:

 $(\mathbf W ~ \PP_n)$ $:$ If $t_1, \ldots, t_n$ are terms, and $p \in \PP_n$ is an $n$-ary predicate symbol, then $\map p {t_1, t_2, \ldots, t_n}$ 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 $\paren {\mathbf A \circ \mathbf B}$ is a WFF $(\mathbf W ~ \forall, \exists)$ $:$ If $\mathbf A$ is a WFF and $x$ is a variable, then $\paren {\forall x: \mathbf A}$ and $\paren {\exists x: \mathbf A}$ are WFFs.