On the predicate logics of finite Kripke frames (Q1344873)

The intermediate predicate logic characterized by the class of all finite Kripke frames (Lfin) is studied. Beforehand by the same author, it is proved that Lfin is not recursively axiomatizable, but that Lfin is \(\Pi^0_2\)-arithmetical. On the other hand, Lfin can be expressed as the intersection of the logics \(\text{LB}_n \text{P}^+_m\), which are characterized by all posets of finite height \(\leq m\) and finite branching \(\leq n\), and which are obviously finitely axiomatizable. Further, the logic \(\text{LP}^+_m\), which is characterized by all posets of height \(\leq m\), is known to be finitely axiomatizable. In this paper, it is proved that \(\text{LB}_n \text{P}^+_m= (\text{LP}^+_m+ \text{B}_n)\), where \(\text{B}_n\) is the propositional axioms of branching \(\leq n\).