next up previous
Next: Hilbert-type system Up: The Formal Systems Previous: Languages

Well formed formulas

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

(W1) tex2html_wrap_inline346,

(W2) tex2html_wrap_inline348,

(W3) tex2html_wrap_inline347,

(W4) tex2html_wrap_inline352.

The symbols tex2html_wrap_inline354 and tex2html_wrap_inline356 denote false and implication, respectively.

We will make use of the following abbreviations:


For any tex2html_wrap_inline410, we define tex2html_wrap_inline412 inductively as follows:

(S1) tex2html_wrap_inline414

(S2) tex2html_wrap_inline416

(S3) tex2html_wrap_inline418

We say tex2html_wrap_inline362 is a subformula of tex2html_wrap_inline360 if tex2html_wrap_inline424.

Yasuko Kitajima
Fri Jun 20 13:39:43 PDT 1997