  So, if we want to eliminate the non-constructive proofs without destroying the symmetry of the sequent calculus, as is done in intuitionistic logic, we can try to eliminate the contraction and weakening rules instead. In doing so, we are left with two different versions of each connective: an additive version and a multiplicative version of conjunction and of disjunction. These different versions of the same connecitve are now no longer equivalent. These new connectives are &amp; (“with”, additive and), \(\oplus\) (“plus”, additive or, \(\otimes\) (“tensor”, multiplicative and) and \(\lpar\) (“par”, multiplicative or).