\begin{definition}[Definition:Language of Propositional Logic/Formal Grammar/WFF]
Let $\mathbf A$ be approved of by the formal grammar of propositional logic.
Then $\mathbf A$ is called a '''well-formed formula of propositional logic'''.
Often, one abbreviates "well-formed formula", speaking of a '''WFF of propositional logic''' instead.
More informally, a '''WFF of propositional logic''' is any sequence of symbols containing statement variables, such that when statements are substituted for the statement variables (the same statement for any given statement variable throughout), the result is a statement.
\end{definition}