The set of well formed formulas is defined to be the least set Wff such that:
The symbols and denote false and implication, respectively.
We will make use of the following abbreviations:
For any , we define inductively as follows:
We say is a subformula of if .