Dual counterpart intuitionistic logic

We introduce dual counterpart intuitionistic logic (or DCInt): a constructive logic that is a conservative extension of intuitionistic logic, a sublogic of bi-intuitionistic logic, has the logical duality property of classical logic, and also retains the modal character of its interpretation of the connective dual to intuitionistic implication. We define its Kripke semantics along with the corresponding notion of a bisimulation, and then prove that it has both the disjunction property and (its dual) the constructible falsity property. Also, for any class $ {\mathcal{C}}$ of Kripke frames from our semantics, we identify a condition such that $ {\mathcal{C}}$ will have the disjunction property if it satisfies the condition. This provides a method for generating extensions of DCInt that retain the disjunction property.