ИСТИНА

We call a formula strictly positive if it is built up of propositional variables, conjunction and modal diamond operators. The strictly positive fragment (SP-fragment) of a logic L is the set of all provable in L implications A->B, where A and B are strictly positive formulas. Evgeny Dashkov proved that the Gödel-Löb provability logic GL and the logic K4 have the same SP-fragments. We study the SP-fragment of the logic K4.3 of all transitive linear frames. We give two different semantic characterizations of the fragmet. We will present a finite axiomatization of the SP-fragment of K4.3 and prove that it is polytime decidable.