How to use a bottom-up grammar to check whether a sentence is well-formed? 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?

 A: 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.

*

*$Q$ and $R$ are WFFs by $W_2$.

*$(Q\lor R)$ is a WFF by (1) and $W_4$.

*$P$ is a WFF by $W_1$.

*$(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.
