I was browsing this set of lecture notes for a mathematical introduction to modal logic. I'm not familiar with model theory, and the lecturers (who approach modal logic from a model-theoretic perspective) recursively define the well-formed formulae of propositional unimodal logic $\mathcal{L}$ as $$\varphi::= p \; \vert \; \top \; \vert \neg \varphi \; \vert \; \varphi \wedge \varphi \; \vert \; \Diamond\varphi$$
where $p$ varies over a countable set $P = \{ p, q, r ... \}.$ This is described as "the signature of propositional logic with the modal operator" which is fine and dandy. I understand 99% of this -- I know what a wff is, what a countable set is, what each of the symbols entail in logical expressions. What I don't know is exactly how the "signature" here works in a rigorous sense. Googling doesn't really help and I can't find anything of a similar notation or structure (to be fair, I don't know where to look or even what to search for.) I can understand intuitively what this means (I think!) -- $p$ is a wff, therefore so is $p \wedge p$, so is $\Diamond p$; and therefore so is $\top(p\wedge p)$, and $\neg \Diamond p$ and so on. I've just never encountered this way of defining a language and it seems so intuitive and useful I would very much like to know more.