We now define the modal system KT5. The axiom schemata for KT5 are as follows:
(A1) 
(A2) 
(A3) 
(A4) 
(A5) 
(A6) 
,
where 
(A7) 
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 
.