\begin{definition}[Definition:Language of Propositional Logic]
There are a lot of different formal systems expressing propositional logic.
Although they vary wildly in complexity and even disagree (to some extent) on what expressions are valid, generally all of these use a compatible formal language.
This page defines the formal language of choice on {{ProofWiki}}.
We will use $\LL_0$ to represent the formal language of propositional logic in what follows.
In order to define $\LL_0$, it is necessary to specify:
* An alphabet $\AA$
* A collation system with the unique readability property for $\AA$
* A formal grammar (which determines the WFFs of $\LL_0$)
{{transclude:Definition:Language of Propositional Logic/Alphabet
  |section = tc
  |title = Alphabet
  |header = 3
  |link = true
  |increase = 1
}}
\end{definition}