How to denote the BNF syntax of propositional calculus?

Question

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$?

---

Hi,

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.

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.