Definition:Language of Propositional Logic/Formal Grammar/Backus-Naur Form

From ProofWiki
Jump to navigation Jump to search


Part of specifying the language of propositional logic is to provide its formal grammar.

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.