We now define the modal system KT5. The axiom schemata for KT5 are as follows:
(A6) , where
We have the following two inference rules:
We write if there exists a proof of . For any we write if for some . is said to be consistent if .