Definition:Language of Propositional Logic/Formal Grammar/Backus-Naur Form
< Definition:Language of Propositional Logic | Formal Grammar(Redirected from Definition:BNF Specification of Propositional Logic)
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
- 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $2$: Propositional Calculus: $\S 2.2$: Propositional formulas: Definition $2.2.1$
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.3$: Propositional logic as a formal language
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.1.6$: Definition $2.13$