Ancestral Kripke Models and Nonhereditary Kripke Models for the Heyting Propositional Calculus

Abstract This is a sequel to two previous papers, where it was shown that, for the Heyting propositional calculus H, we can give Kripke-style models whose accessibility relation R need not be a quasi-ordering relation, provided we have: x\=A &Vy(xRy= * y VA). From left to right, this is the heredity condition of standard Kripke models for H, but, since R need not be reflexive, the converse is not automatically satisfied. These Kripke-style models for H were called "rudimentary Kripke models". This paper introduces a kind of dual of rudimentary Kripke mod-els, where the equivalence above is replaced by: x^A <#3y(yRx &y \=A). From right to left, this is again the usual heredity condition, but the converse, which is automatically satisfied if R is reflexive, yields a proper subclass of rudimentary Kripke models, whose members are called "ancestral Kripke models". In all that, the semantic clauses for the connectives are as in stan-dard Kripke models for H. The propositional calculus H is strongly sound and complete with respect to ancestral Kripke models. The remainder of the paper is devoted to Kripke-style models for H where the semantic clauses for the connectives are changed so that we need not assume any of the heredity conditions above. The resulting Kripke-style models are called "nonhereditary Kripke models". These models are inspired by some particular embeddings of H into 54 and a somewhat weaker normal modal logic. With respect to a notion of quasi-ordered nonhereditary Kripke model, we can prove a certain form of strong soundness and completeness of H. With respect to another notion, where quasi-ordering is not assumed, we can only prove the ordinary soundness and completeness of H