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

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

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