Definition:Language of Predicate Logic/Formal Grammar

From ProofWiki
Jump to navigation Jump to search

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.             


Sources