Well formed formulas

The set of well formed formulas is defined to be the least set Wff such that:

(W1) ,

(W2) ,

(W3) ,

(W4) .

The symbols and denote false and implication, respectively.

We will make use of the following abbreviations:

For any , we define inductively as follows:

(S1)

(S2)

(S3)

We say is a subformula of if .