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

From ProofWiki
Jump to navigation Jump to search

Definition

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 \meta {formula}\) \(\)::=\(\) \(\ds p \ \mid \ \top \ \mid \ \bot\) where $p \in \PP_0$ is a letter
\(\ds \meta {formula}\) \(\)::=\(\) \(\ds \neg \meta {formula}\)
\(\ds \meta {formula}\) \(\)::=\(\) \(\ds (\meta {formula} \ \meta {op} \ \meta {formula})\)
\(\ds \meta {op}\) \(\)::=\(\) \(\ds \land \ \mid \ \lor \ \mid \implies \mid \iff\)


Note that this is a top-down grammar:

we start with a metasymbol $\meta {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.


Sources