next up previous
Next: Completeness of KT5-models Up: Kripke-type Semantics Previous: Definition of Kripke-type models

Soundness of KT5-models

We now wish to show that each formula provable in KT5 is valid in any KT5-model.

Theorem 1. (Soundness Theorem) If tex2html_wrap_inline446 then tex2html_wrap_inline508 for any KT5-model M.

Corollary 2. (Consistency of KT5) tex2html_wrap_inline354 is not provable in KT5.

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