tldr: how to design a BNF grammar for propositional calculus acknowledging the order of precedence between different logical connectives and disallowing stuff like $p \lor q \land r$?


lately I’ve been thinking about the (E)BNF notation for syntax for different areas and I’ve thought about the propositional calculus. How to define a BNF syntax for it? I know that for simple arithmetic expressions (even excluding binary minus and division but those are analoguous to + and *) we could use something like that

<expression> ::= <term> + <expression> | <term>
<term> ::= - <term> | <factor> * <term>
<factor> ::= (<expression>) | <number>

and one could think that logical connectives sort of resemble those operators above but there are some differences right? Eg. when I googled for a BNF syntax for logic I found some that are very simple like here and completely ignore the precedence order.

So as I was taught the precedence order is:

  1. negation
  2. conjunction and disjunction (they are equally important)
  3. implication and equivalence

When compared to the syntax designed for arithmetic above we see that the unary minus is exactly like negation but addition doesn't map to disjunction So what I always thought was that a formula like $p \wedge q \vee r$ is illegal since it is not clear whether it is $(p \wedge q) \vee r$ or $p \wedge (q \vee r)$ (yet another reason for choosing polish for logic) but I do not know how to define a syntax that would make these not show up in the production process. I've seen BNFs for logic online which simply ignored that or assumed that $\wedge$ takes precedence over $\vee$ for which there is no real reason in my opinion since both are distributive (contrary to multiplication and addition as in the first example out of which only one is).

So how to define such a syntax using simple BNF rules?

edit: ok so clearly I wasn't precise enough and that's my bad. So the model for propositional calculus I was taught and which I believe is quite logical is to apply the order of precedence as listed above. About associativity... I haven't given it much thought to be frank and personally I'd bracket stuff like $p \to q \to r$ since it has two interpretations that are not equivalent and I don't really know which one would be the obvious one. But for other connectives the parentheses are not necessary since we have tautologies like $((p\lor q) \lor r) \leftrightarrow (p \lor (q \lor r))$ (the same follows for conjunction and equivalence) hence we see that we don't need to add any parentheses there. But as I said I am not so sure about this one.

But there is some confusion below about the order of precedence. So as I've said above I consider disjunction having a higher order of precedence than implication etc. So a formula like $\lnot p \lor q \to r$ is to be interpreted as $((\lnot p) \lor q) \to r$.

The whole issue I am having is with the disjunction and conjunction mix where I don't consider $p \lor q \land r$ to be a well formed formula.

  • $\begingroup$ How about $p \lor q \lor r$? Or $p \to q \to r$? You need to be clear about these issues before you design your language and your grammar. (Asides: taking $\land$ to have prior precedence from $\lor$ has a long history: Boole wrote conjunction as multiplication and disjunction as addition. It is often better for everyone concerned to use an ambiguous grammar and to define operator precedence and associative rules separately.) $\endgroup$
    – Rob Arthan
    Feb 23, 2021 at 23:21
  • 1
    $\begingroup$ I mentioned issues with associativity above. These show up in your example BNF grammar for arithmetic expressions: it would give counterintuitive results if you treated binary $-$ in the same way as binary $+$: we expect $3 - 2 - 1$ to mean $(3 - 2) - 1 = 0$ not $3 - (2 - 1) = 2$. The mathematical logic community is apparently divided on what $p \to q \to r$ should mean, but the computer science community (and many mathematicians) expect it to mean $p \to (q \to r)$ rather than $(p \to q) \to r$. $\endgroup$
    – Rob Arthan
    Feb 23, 2021 at 23:45
  • $\begingroup$ I can see that. I have tried to tackle this issue with an edit but to summarise it $p \vee q \vee r$ is totally ok since no matter how we'd put the parentheses it would mean the same. For implication it is not true $\endgroup$
    – ggegoge
    Feb 24, 2021 at 9:30

1 Answer 1


The crucial point is to require external parentheses for every binary connective, so that priority between binary connectives is unambiguous.

Formally, given a (usually countably infinite) set of atomic formulas, the BNF syntax of formulas of propositional calculus is the following:

\begin{align*} \langle \text{formula} \rangle &::= \langle \text{atomic} \rangle \mid \lnot \langle \text{formula} \rangle \mid (\langle \text{formula} \rangle \land \langle \text{formula} \rangle) \\ &\quad \mid (\langle \text{formula} \rangle \lor \langle \text{formula} \rangle) \mid (\langle \text{formula} \rangle \to \langle \text{formula} \rangle) \end{align*}

Note that this means that, given some atoms $p$, $q$ and $r$, the strings $p \land q$ and $p \lor q \land r$ and $p\lor (q \land r)$ are not formulas. On the contrary, the strings $(p \land q)$ and $((p \lor q) \land r)$ and $(p\lor (q \land r))$ are formulas.

  • $\begingroup$ That doesn't achieve what the OP wants. The OP wants to accept $p \to q \lor r$ as correct and meaning what your grammar would have to express as $(p \to (q \lor r))$ but to require the parentheses in $p \land (q \land r)$. $\endgroup$
    – Rob Arthan
    Feb 23, 2021 at 23:13
  • $\begingroup$ @RobArthan - I don't think that the OP wants to accept $p \to q \lor r$. Quoting from the OP: "how to design a BNF grammar for propositional calculus [...] disallowing stuff like $ p \lor q \land r$?". Do I miss something? $\endgroup$ Feb 23, 2021 at 23:18
  • $\begingroup$ You missed the part of the question where the OP lists the precedence order that he or she has been taught and wants to apply. $\endgroup$
    – Rob Arthan
    Feb 23, 2021 at 23:23
  • 1
    $\begingroup$ @RobArthan - I'm not sure that the fact to accept $p \to q \lor r$ as a formula is mandatory in the OP. I hope the OP's author can clarify what they exactly want. $\endgroup$ Feb 23, 2021 at 23:37
  • $\begingroup$ The question does need clarification. But the only point about talking about a precedence order is to allow some brackets to be omitted. $\endgroup$
    – Rob Arthan
    Feb 23, 2021 at 23:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .