**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

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.

Last revised on October 3, 2023 at 05:51:23. See the history of this page for a list of all contributions to it.