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
.

Fri Jun 20 13:39:43 PDT 1997