Contrapositionally complemented Heyting algebras and intuitionistic logic with minimal negation.

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally |$\vee $| complemented Heyting algebra (c |$\vee $| 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 ccHa s and its extension |${\textrm {ILM}}$| - |${\vee }$| for c |$\vee $| cHa s 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 |${\textrm {ILM}}$| - |${\vee }$| are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and |${\textrm {ILM}}$| - |${\vee }$| 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 |$K_{im-{\vee }}$| are discussed, where the language does not include implication. The |$K_{im}$| -algebras are reducts of ccHa s and are different from relevant algebraic structures having two negations. The negations in the |$K_{im}$| -algebras and |$K_{im-{\vee }}$| -algebras are shown to occupy distinct positions in an enhanced form of Dunn's kite of negations. Relational semantics for |$K_{im}$| and |$K_{im-{\vee }}$| 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 |${\textrm {ILM}}$| - |${\vee }$|⁠. [ABSTRACT FROM AUTHOR]