# How complex are natural deduction proofs compared to sequent calculus proofs without cut?

A complete answer to your question is likely to depend on the details of the particular natural deduction system and sequent proof system that you have in mind. In general, sequent systems with cut tend to be rather similar to natural deduction systems. Specifically, given a natural deduction system, one can set up a closely related sequent calculus, in which a sequent $\Gamma\implies\phi$ is provable if and only if the natural deduction system has a proof of $\phi$ with open (i.e., undischarged or uncanceled, depending on your terminology) assumptions $\Gamma$. In this situation, I would expect the complexity of sequent proofs and of natural deduction proofs to be very similar. A proof, or even a careful formulation of that fact would require looking closely at the axioms and rules of both systems, to see how closely each one simulates the other.