Why is a cut-free system consistent?

Question

Assume that the cut-elimination theorem holds for a system $T$. Then, for any proof that makes use of the cut-rule in $T$, there is a proof that does not make use of the cut-rule. An immediate corollary of it is that if there is a proof of the sequent $\Rightarrow \bot$, there is a cut-free proof of the absurd. Then the usual conclusion is that $T$ is consistent. But I wonder why it is so natural that there is a cut-free proof of the absurd in $T$? In other words,

Why is that the cut-elimination rule implies consistency of a logical system?

For dependently typed theories, cut-elimination corresponds to (strong) normalization. It is easier for me to see the argument from this viewpoint: if every term of a dependently typed theory reduces in a finite steps to a normal form, and there is no canonical inhabitant of the False type, then, it goes without saying that the theory is consistent, i.e. there are no inhabitants of the False.

But how is that the argument is given in the general context of cut-elimination?

Answer 1

For the Gentzen sequent calculus, cut-free proofs have the subformula property: every formula that occurs in a proof of $\Gamma \Rightarrow \Delta$ is a subformula of an element of $\Gamma\cup\Delta$. Indeed, the cut-rule is the only rule that doesn't have this property. It follows immediately that there is no cut-free derivation of the contradictory sequent $\varnothing \Rightarrow \varnothing$.