next up previous
Next: Kripke-type Semantics Up: The Formal Systems Previous: Well formed formulas

Hilbert-type system

We now define the modal system KT5. The axiom schemata for KT5 are as follows:

(A1) tex2html_wrap_inline428

(A2) tex2html_wrap_inline427

(A3) tex2html_wrap_inline429

(A4) tex2html_wrap_inline434

(A5) tex2html_wrap_inline436

(A6) tex2html_wrap_inline438, where tex2html_wrap_inline437

(A7) tex2html_wrap_inline442

We have the following two inference rules:
We write tex2html_wrap_inline446 if there exists a proof of tex2html_wrap_inline360. For any tex2html_wrap_inline450 we write tex2html_wrap_inline452 if tex2html_wrap_inline454 for some tex2html_wrap_inline456. tex2html_wrap_inline458 is said to be consistent if tex2html_wrap_inline460.

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