Definition:Language of Propositional Logic/Formal Grammar

From ProofWiki
Jump to navigation Jump to search

Definition

The formal grammar of the language of propositional logic (and hence its WFFs) can be defined in the following ways.


Backus-Naur Form

In Backus-Naur form, the formal grammar of the language of propositional logic takes the following form:


\(\displaystyle \)<formula>\(\) \(\)::=\(\) \(\displaystyle p \ \mid \ \top \ \mid \ \bot\) where $p \in \mathcal P_0$ is a letter
\(\displaystyle \)<formula>\(\) \(\)::=\(\) \(\displaystyle \neg\) <formula>\(\)
\(\displaystyle \)<formula>\(\) \(\)::=\(\) \(\displaystyle (\) <formula> <op> <formula> \()\)
\(\displaystyle \)<op>\(\) \(\)::=\(\) \(\displaystyle \land \ \mid \ \lor \ \mid \implies \mid \iff\)


Note that this is a top-down grammar: we start with a metasymbol <formula> and progressively replace it with constructs containing other metasymbols and/or primitive symbols, until finally we are left with a well-formed formula of $\mathcal L_0$ consisting of nothing but primitive symbols.


Bottom-Up Specification

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


  • Let $\mathcal P_0$ be the vocabulary of $\mathcal L_0$.
  • Let $Op = \left\{{\land, \lor, \implies, \iff}\right\}$.


The rules are:

$\mathbf W: TF$ $:$ $\top$ is a WFF, and $\bot$ is a WFF.
$\mathbf W: \mathcal P_0$ $:$ If $p \in \mathcal P_0$, then $p$ is a WFF.
$\mathbf W: \neg$ $:$ If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF.
$\mathbf W: Op$ $:$ If $\mathbf A$ is a WFF and $\mathbf B$ is a WFF and $\circ \in Op$, then $\left({\mathbf A \circ \mathbf B}\right)$ is a WFF.


Any string which can not be created by means of the above rules is not a WFF.


Well-Formed Formula

Let $\mathbf A$ be approved of by the formal grammar of propositional logic.


Then $\mathbf A$ is called a well-formed formula of propositional logic.

Often, one abbreviates "well-formed formula", speaking of a WFF of propositional logic instead.


Also known as

The formal grammar of propositional logic is also referred to as its syntax.


Also see


Sources