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)

Recent studies in semantics of modal and superintuitionistic predicate logics provided many examples of incompleteness, especially for Kripke semantics. So there is a problem: to find an appropriate possible- world semantics which is equivalent to Kripke semantics at the propositional level and which is strong enough to prove general completeness results. The present paper introduces a new semantics of Kripke metaframes' generalizing some earlier notions. The main innovation is in considering "n"-tuples of individuals as abstract "n"-dimensional vectors', together with some (...) transformations of these vectors. Soundness of the semantics is proved to be equivalent to some non- logical properties of metaframes; and thus we describe the maximal semantics of Kripke- type. (shrink)

The Kripke-completeness and incompleteness of some intermediate predicate logics is established. In particular, we obtain a Kripke-incomplete logic (H* +A+D+K) where H* is the intuitionistic predicate calculus, A is a disjunction-free propositional formula, D = x(P(x) V Q) xP(x) V Q, K = ¬¬x(P(x) V ¬P(x)) (the negative answer to a question of T. Shimura).

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)

We generalize the incompleteness proof of the modal predicate logic Q-S4+ p p + BF described in Hughes-Cresswell [6]. As a corollary, we show that, for every subframe logic Lcontaining S4, Kripke completeness of Q-L+ BF implies the finite embedding property of L.

This chapter contains sections titled: Introduction Modal propositional Logics (MPLs) Modal Quantificational Logics(QMLs).

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.