\begin{definition}[Definition:Definitional Abbreviation]
When discussing a formal language, some particular WFFs may occur very often.
If such WFFs are very unwieldy to write and obscure what the author tries to express, it is convenient to introduce a shorthand for them.
Such a shorthand is called a '''definitional abbreviation'''.
It does ''not'' in any way alter the meaning or formal structure of a sentence, but is purely a method to keep expressions readable to human eyes.
\end{definition}