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)

In so-called Kripke-type models, each sentence is assigned either to true or to false at each possible world. In this setting, every possible world has the two-valued Boolean algebra as the set of truth values. Instead, we take a collection of algebras each of which is attached to a world as the set of truth values at the world, and obtain an extended semantics based on the traditional Kripke-type semantics, which we call here the algebraic Kripke semantics. We introduce algebraic (...) Kripke sheaf semantics for super-intuitionistic and modal predicate logics, and discuss some basic properties. We can state the Gödel-McKinsey-Tarski translation theorem within this semantics. Further, we show new results on super-intuitionistic predicate logics. We prove that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties and moreover the same propositional fragment as the intuitionistic logic. (shrink)

A method for constructing continua of logics squeezed between some intermediate predicate logics, developed by Suzuki [8], is modified and applied to intervals of the form [L, L+ ¬¬S], where Lis a predicate logic, Sis a closed predicate formula. This solves one of the problems from Suzuki's paper.

We propose a new, rather simple and short proof of Kripke-completeness for the predicate variant of Dummett's logic. Also a family of Kripke-incomplete extensions of this logic that are complete w.r.t. Kripke frames with equality (or equivalently, w.r.t. Kripke sheaves [8]), is described.

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)

An intermediate predicate logicS + n (n>0) is introduced and investigated. First, a sequent calculusGS n is introduced, which is shown to be equivalent toS + n and for which the cut elimination theorem holds. In § 2, it will be shown thatS + n is characterized by the class of all linear Kripke frames of the heightn.