\begin{definition}[Definition:Language of Propositional Logic/Formal Grammar/Backus-Naur Form]
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:
{{begin-eqn}}
{{eqn | l = \)<tt><formula></tt>\(
      | o = \)<tt>::=</tt>\(
      | r = p \ \mid \ \top \ \mid \ \bot
      | c = where $p \in \PP_0$ is a letter
}}
{{eqn | l = \)<tt><formula></tt>\(
      | o = \)<tt>::=</tt>\(
      | r = \neg\) <tt><formula></tt>\(
}}
{{eqn | l = \)<tt><formula></tt>\(
      | o = \)<tt>::=</tt>\(
      | r = (\) <tt><formula></tt> <tt><op></tt> <tt><formula></tt> \()
}}
{{eqn | l = \)<tt><op></tt>\(
      | o = \)<tt>::=</tt>\(
      | r = \land \ \mid \ \lor \ \mid \implies \mid \iff
}}
{{end-eqn}}
Note that this is a top-down grammar:
:we start with a metasymbol <tt><formula></tt>
: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.
\end{definition}