Such a grammar can be made explicit by declaring that:
- A metasymbol may be replaced by certain collations labeled with metasymbols and signs of $\mathcal A$.
- Letters are well-formed formulas.
- A collection of specified collations of well-formed formulas, possibly labeled with additional signs, are also well-formed formulas.
In certain use cases, the first clause is adjusted to allow for more complex situations, for example in the bottom-up specification of predicate logic
Also known as
Some sources call this merely a grammar, the term formal being taken for granted by the fact that a formal language is under discussion.