nLab subformula property

Idea

The subformula property is a property of cut-free presentations of the sequent calculus. It says that in any derivation

$$\frac{\vdots}{\Gamma\vdash \Delta}$$

any type appearing above the line is a subformula of one of the types appearing in $\Gamma,\Delta$. This makes it easy to make arguments about provability: while it is not obvious in a cut-full system that the contradiction/empty sequent $\cdot\vdash\cdot$ is not derivable, it is a corollary of the subformula property that $\cdot \vdash \cdot$ is not derivable because all of the rules of the cut-free calculus involve a type below the line.

This property is a formal expression of the modularity of type theoretic connectives: each connective is given by rules which involve only its arguments.