Finite trees in tense logic

From MaRDI portal
(Redirected from Finite trees in tense logic)





The paper studies tense logics of finite trees. The minimal logic of this kind (denoted by \(L_1\)) is obtained from the minimal tense logic \(K_t\) by adding transitivity, Löb axioms in both directions and non-branching in the past. It is proved that for the language with \(k\) propositional variables, where \(k\) is finite, isomorphism classes of irreducible Kripke models on finite trees are definable; a Kripke model is called irreducible iff all its generated submodels are non-isomorphic. This implies that two distinguishable Kripke models on finite trees are isomorophic iff they are modally equivalent. Also it is proved that every tense logic of a finite tree has an (effective) weakly minimal finite axiomatization over \(L_1\); the weak minimality means that it uses the minimal number of variables and in \(L_1\) it implies any other axiomatization in the same variables. Another result is that the lattice of extensions of \(L_1\) has \(2^{\aleph_0}\) coatoms, as it is for extensions of \(K_t\). Finally, the paper proves that for logics of this kind adding `Until' and `Since' does not increase the expressive power: two finite trees are equivalent in tense logic iff they are equivalent in Until-Since logic.











This page was built for publication: Finite trees in tense logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1288959)