The completeness w.r.t. Kripke frames with equality (or, equivalently, w.r.t. Kripke sheaves, [ 8 ] or [4, Sect. 3.6]) is established for three superintuitionistic predicate logics: ( Q - H + D *), ( Q - H + D *&K), ( Q - H + D *& K & J ). Here Q - H is intuitionistic predicate logic, J is the principle of the weak excluded middle, K is Kuroda’s axiom, and D * (cf. [ 12 ]) is a (...) weakened version of the well-known constant domains principle D . Namely, the formula D states that any individual has ancestors in earlier worlds, and D * states that any individual has $${\neg\neg}$$ -ancestors (i.e., ancestors up to $${\neg\neg}$$ -equality) in earlier worlds. In particular, the logic ( Q - H + D *& K & J ) is the Kripke sheaf completion of ( Q - H + E & K & J ), where E is a version of Markov’s principle (cf. [ 12 ]). On the other hand, we show that the logic ( Q - H + D *& J ) is incomplete w.r.t. Kripke sheaves. (shrink)

In [Ono 1987] H. Ono put the question about axiomatizing the intermediate predicate logicLFin characterized by the class of all finite Kripke frames. It was established in [ Skvortsov 1988] thatLFin is not recursively axiomatizable. One can easily show that for any finite posetM, the predicate logic characterized byM is recursively axiomatizable, and its axiomatization can be constructed effectively fromM. Namely, the set of formulas belonging to this logic is recursively enumerable, since it is embeddable in the two-sorted classical predicate (...) calculusCPC 2. Thus the logicLFin is II 2 0 -arithmetical.Here we give a more explicit II 2 0 -description ofLFin: it is presented as the intersection of a denumerable sequence of finitely axiomatizable Kripke-complete logics. Namely, we give an axiomatization of the logicLB n P m + characterized by the class of all posets of the finite height m and the finite branching n. A finite axiomatization of the predicate logicLP m + characterized by the class of all posets of the height m is known from [Yokota 1989]. We prove thatLB n P m + =,B n being the propositional axiom of the branching n. (shrink)