We compare the logic HYPE recently suggested by H. Leitgeb as a basic propositional logic to deal with hyperintensional contexts and Heyting-Ockham logic introduced in the course of studying logical aspects of the well-founded semantics for logic programs with negation. The semantics of Heyting-Ockham logic makes use of the so-called Routley star negation. It is shown how the Routley star negation can be obtained from Dimiter Vakarelov’s theory of negation and that propositional HYPE coincides with the logic characterized by the (...) class of all involutive Routley star information frames. This result provides a much simplified semantics for HYPE and also a simplified axiomatization, which shows that HYPE is identical with the modal symmetric propositional calculus introduced by G. Moisil in 1942. Moreover, it is shown that HYPE can be faithfully embedded into a normal bi-modal logic based on classical logic. Against this background, we discuss the notion of hyperintensionality. (shrink)

The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...) some special forms can be eliminated from a proof in LD. From these cut-elimination theorems we obtain some corollaries on syntactical properties of CD: fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD. (shrink)