Algebraic Kripke sheaf semantics for non-classical predicate logics

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.