# nLab subformula property

Subformula property

# 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 that a cut-full system that the contradiction/empty sequent $\cdot\vdash\cdot$ is derivable, it is a corollary of the subformula property that the $\cdot \vdash \cdot$ is not derivable because all of the rules of the cut-free calculus involve a type above 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.

Created on January 25, 2018 at 11:23:27. See the history of this page for a list of all contributions to it.