Contrapositionally complemented Heyting algebras and intuitionistic logic with minimal negation

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally boolean OR complemented Heyting algebra (c boolean OR cHa), are studied. The salient feature of these algebras is that there are two negations, one intuitionistic and another minimal in nature, along with a condition connecting the two operators. Properties of these algebras are discussed, examples are given and comparisons are made with relevant algebras. Intuitionistic Logic with Minimal Negation (ILM) corresponding to ccHas and its extension ILM-boolean OR for c boolean OR cHas are then investigated. Besides its relations with intuitionistic and minimal logics, ILM is observed to be related to Peirce's logic and Vakarelov's logic MIN. With a focus on properties of the two negations, relational semantics for ILM and ILM-boolean OR are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and ILM-boolean OR are shown to have the finite model property with respect to these classes of frames and proved to be decidable. Extracting features of the two negations in the algebras, a further investigation is made, following logical studies of negations that define the operators independently of the binary operator of implication. Using Dunn's logical framework for the purpose, two logics K-im and Kim-boolean OR are discussed, where the language does not include implication. The K-im-algebras are reducts of ccHas and are different from relevant algebraic structures having two negations. The negations in the K-im-algebras and Kim-boolean OR-algebras are shown to occupy distinct positions in an enhanced form of Dunn's kite of negations. Relational semantics for K-im and Kim-boolean OR is provided by a class of frames that are based on Dunn's compatibility frames. It is observed that this class coincides with one of the four classes giving the relational semantics for ILM and ILM-boolean OR .