contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら，シーケント計算の推論規則を

  • ∧右，∨左，⊃左は additive
  • ∧左，∨右 は multiplicative

にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いような気がしますが，Wang's algorithm に対応するように推論規則を作るとこうなるようです。

一階述語論理では反例があって， \exists x ( (P(a) \land P(b) ) \lor \neg P(x) ) は contraction がないと証明できないようです。∃右規則を

\displaystyle{ \frac{\Gamma \Rightarrow \Delta, A[t_1], \dots, A[t_n]}{\Gamma \Rightarrow \Delta, \exists xA[x]} }

として，∀左も同様に変更すると contraction なしで済みそうですが（確認してないけど）。

これは一体，何を意味するのだろうか。