We present a logical calculus extending the classical propositional calculus with an additional connective which has some features of substructural logic. This results in a logic which seems to be suitable for reasoning with ambiguity. We use a Gentzen style proof theory based on multi-contexts, which allow us to have two ways to combine formulas to sequences. These multi-contexts in turn allow to embed both features of classical logic as well as substructural logic, depending on connectives, which would be impossible with simple sequents. Finally, we present an algebraic semantics and a completeness theorem.
展开▼