Gabbay has pointed out a difficulty with the bring methodology for combining logics that became known as the collapsing problem. The argument given suggested that there would be no way of combining classical and intuitionistic propositional logics, CPL and IPL respectively, in a way that would not collapse the intuitionistic connectives into classical ones.

Following this spirit, Andreas Herzig and Luis Fari~nas del Cerro have proposed a combined logic C+J that starts from the expected combined semantic setting, that could be axiomatized, not by adding the axiomatizations of CPL and IPL together with some interaction rules, but rather by modifying these axioms along with their scope of applicability.

We propose a new logic, inspired by the problems above, encompassing both classical and intuitionistic propositional logics. A preliminary step towards this logic was already taken by considering a combination of the implicative fragments of CPL and IPL, that was shown to be a conservative extension of both logics. The design of this logic is based on the key idea of keeping at the core of the deductive system the axioms and rules of both logics. As it would be expected, since we are aiming at a complete axiomatization, some extra axioms are needed to express the existing interaction between the two logics. For instance, intuitionistic implication is weaker than classical implication and this fact needs to be expressed in the logic. Still, these interaction axioms are carefully chosen to guarantee that the two logics do not collapse. The semantics for the logic was inspired by the semantic models obtained by cryptobring. In this case, we adopt as models for the logic the usual Kripke model for intuitionistic logic. The semantic for the classical connectives over these models needs to be defined with care as to ensure that the usual semantics is preserved. The resulting logic is then proved to sound and complete and, furthermore, it is proved to extended conservatively both classical and intuitionistic propositional logics.

The logic is also shown to be decidable. To this end, we introduce a tableau system based on labeled formulas. We consider two kinds of labels. One of these labels concerns the truth value of the formula, that can be either true or false.
The other one denotes the world (of the intended Kripke model) in which the formula is being evaluated. Each labeled formula will have one of each of these two labels. Due to the nature of the intuitionistic implication, the set of labels
for the worlds cannot be arbitrary. In particular, we need it to be nite in order keep our tableaux nite. Hence, we consider a (nite) set of world labels, that is build up based on the formula that is being considered, where each label has
a semantic avor attached to it.

Another competing approach was recently proposed by Liang and Miller for intuitionistic and classical first order logics. Though diferent in spirit, it seems worth understanding its connection to our approach