[Proof Complexity] A New Preprint

[Amir Tabatabai]

Dear all,

I am happy to share our new preprint, “Proof Complexity of Linear Logics”:

https://arxiv.org/abs/2601.22393

In this work, we study the role of structural rules in the proof complexity
of the sequent system LK for classical logic (equivalently, the Frege
system). More precisely, we establish exponential separations between LK
and its subsystems that lack either contraction or weakening. We also show
that the combination of these two rules without cut is exponentially weaker
than the cut rule on its own. This investigation of structural rules can be
seen as a natural extension of Jan Krajíček’s result separating LK from its
cut-free fragment.

Comments, suggestions, and corrections are most welcome.

Best wishes,
Amir.