Definition:Language of Predicate Logic/Formal Grammar

From ProofWiki
Jump to navigation Jump to search


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.


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.