The superintuitionistic predicate logics (without or with equality) of all predicate Kripke frames with nested domains over a fixed poset W (a set of possible worlds) are embeddable in the logic (without equality) of all Kripke frames with constant domains over W. Therefore, Takano's result [13] on finite axiomatizability of the logic of Kripke frames with constant domains over the set of real numbers implies the recursive axiomatizability of the corresponding logics with nested domains. Other consequences are mentioned as well.

The article presents general results on non-axiomatizability for superintuitionistic predicate logics. In particular, the logics of all well-ordered, all dually well-ordered, and all dually well-founded Kripke frames (in the semantics with nested and with constant domains) are -hard, and the logic of all Kripke frames of finite height is not recursively axiomatizable (although it is known to be -arithmetical). A result on Kripke-incompleteness is stated as well.

Abstract We prove that an intermediate predicate logic characterized by a class of finite partially ordered sets is recursively axiomatizable iff it is “finite”, i.e., iff it is characterized by a single finite partially ordered set. Therefore, the predicate logic LFin of the class of all predicate Kripke frames with finitely many possible worlds is not recursively axiomatizable.