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

The definition proceeds in two steps.

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


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.