Definition:Language of Propositional Logic/Formal Grammar

From ProofWiki
Jump to navigation Jump to search


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:

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

Note that this is a top-down grammar:

we start with a metasymbol <formula>
progressively replace it with constructs containing other metasymbols and/or primitive symbols

until finally we are left with a well-formed formula of $\LL_0$ consisting of nothing but primitive symbols.

Bottom-Up Specification

The following rules of formation constitute a bottom-up grammar for the formation of well-formed formulas (WFFs) of the language of propositional logic $\LL_0$.

Let $\PP_0$ be the vocabulary of $\LL_0$.
Let $\mathrm {Op} = \set {\land, \lor, \implies, \iff}$.

The rules are:

$\mathbf W: \text {TF}$ $:$ $\top$ is a WFF, and $\bot$ is a WFF.
$\mathbf W: \PP_0$ $:$ If $p \in \PP_0$, then $p$ is a WFF.
$\mathbf W: \neg$ $:$ If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF.
$\mathbf W: \text {Op}$ $:$ If $\mathbf A$ is a WFF and $\mathbf B$ is a WFF and $\circ \in \mathrm {Op}$, then $\paren {\mathbf A \circ \mathbf B}$ 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