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:

\(\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.