Finite trees in tense logic (Q1288959)

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.