On the predicate logics of finite Kripke frames

Abstract

In [Ono 1987] H. Ono put the question about axiomatizing the intermediate predicate logic LFin characterized by the class of all finite Kripke frames (Problem 4,P41). It was established in [Skvortsov 1988] that LFin is not recursively axiomatizable. One can easily show that for any finite poset M, the predicate logic characterized by M is recursively axiomatizable, and its axiomatization can be constructed effectively from M. Namely, the set of formulas belonging to this logic is recursively enumerable, since it is embeddable in the two-sorted classical predicate calculus CPC2 (the definition of the truth in a Kripke model may be expressed by a formula of CPC2). Thus the logic LFin is II20-arithmetical. Here we give a more explicit II20-description of LFin: it is presented as the intersection of a denumerable sequence of finitely axiomatizable Kripke-complete logics. Namely, we give an axiomatization of the logic LBnPm+ characterized by the class of all posets of the finite height ≤m and the finite branching ≤n. A finite axiomatization of the predicate logic LPm+ characterized by the class of all posets of the height ≤m is known from [Yokota 1989] (this axiomatics is essentially first-order; the standard propositional axiom of the height ≤m is not sufficient [Ono 1983]). We prove that LBnPm+=(LPm++Bn), Bn being the propositional axiom of the branching ≤n (see [Gabbay, de Jongh 1974]). Our terminology and notations mainly correspond to [Ono 1987]. © 1995 Kluwer Academic Publishers.