How to use a bottom-up grammar to check whether a sentence is well-formed?

Question

Proofwiki provides a concise description of the language of propositional logic using bottom-up grammar:

Let $\mathcal{P}_0$ be the vocabulary of $\mathcal{L}_0$
Let $\text{Op} = \{\land, \lor, \implies, \iff \}$

The rules are:

$\mathbf W: \text {TF}: \top$ is a WFF, and $\bot$ is a WFF
$\mathbf W: \mathcal{P_0}:$ If $p \in \mathcal{P_0}$, then $p$ is a WFF.
$\mathbf W: \lnot:$ If $\mathbf{A}$ is a WFF, then $\lnot \mathbf A$ is a WFF.
$\mathbf W: \text{Op}:$ If $\mathbf{A}$ is a WFF and $\mathbf{B}$ is a WFF and $\circ \in \text{Op}$, then $(\mathbf{A} \circ \mathbf{B}) $ is a WFF

As far as I understand, WFF stands for "well formed formula". I am not sure what $\mathbf{W}$ stands for but I think it might be analogous to something like a "Nonterminal expression" (in contrast with a "terminal expression"). Basically, this means that the rule corresponds to a node and not a leaf in the abstract syntax tree. The reason I think this may be the case is that the bottom up grammar for $\mathcal{L}_1$ (predicate logic) has a symbol for $\mathbf{T}$ which corresponds to a "Term". I am not sure why the bottom up grammar that I quote above has no terminals defined. Perhaps this is a mistake in the proofwiki page. Perhaps they intended for $\mathcal P_0$ and $\text{Op}$ to be the terminal symbols?

As far as I understand, the alphabet $\mathcal A$ is the union of the vocabulary and the signs. If I had to write this out for a simple set of 3 propositions I would do it as follows:

$$\mathcal P_0 = \{P, Q, R\}$$ $$\mathrm {Op} = \{\land, \lor, \implies, \iff\}$$ $$\mathcal A = \mathcal P_0 \cup \text{Op} = \{P, Q, R, \land, \lor, \implies, \iff\}$$

I do however notice that other signs such as $\top, \bot, \lnot, ($ and $)$ are missing from the alphabet, but they are part of the grammar so perhaps that is sufficient?

In addition, I have two other questions:

• Is my understanding based on the explanation I provide above for the grammar of language $\mathcal L_0$ correct?
• Suppose I have a simple sentence like $(P \land (Q \lor R))$. How can I use the defined grammar to verify whether the sentence is well-formed?

Answer 1

W merely designates those four statements as the rules for forming WWFs; in the description of $\mathscr{L}_1$ it is used the same way, and T is used for the statements defining terms. There should be a fifth statement to the effect that a string of symbols is a WFF if and only if it can be constructed using the previous four statements.

The alphabet is $\mathscr{P}_0\cup\mathrm{Op}\cup\{\top,\bot,\neg,(,)\}$. $\mathrm{Op}$ is just the set of binary connectives; $\neg$ is unary, and $\top$ and $\bot$ are nullary.

To use the grammar to show that $(P\land(Q\lor R))$ is well-formed, you can proceed as follows; I’ve numbered the four W statements $W_1,W_2,W_3$, and $W_4$ in order.

1. $Q$ and $R$ are WFFs by $W_2$.
2. $(Q\lor R)$ is a WFF by (1) and $W_4$.
3. $P$ is a WFF by $W_1$.
4. $(P\land(Q\lor R))$ is a WFF by (2), (3), and $W_4$.

Or you could build a syntax tree like this

                     (P ∧ (Q ∨ R))
                    /             \
                   P            (Q ∨ R)
                               /       \
                              Q         R

and then use the W rules to justify each set of offspring of each node that isn’t a leaf.