  Notice though that once one has eliminated the contraction and weakening rule, formulas no longer behave as immutable truth values: indeed, when we have a proof of \(A \Rightarrow B\) and a proof of \(A\) in linear logic, by composing them we actually consume them to get a proof of \(B\), so that \(A \Rightarrow B\) and \(A\) are no longer available after the composition. Linear logic formulas behave now more like resources that can only be used once.