# Spahn rules of type theories (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

• Bart jacobs, Categorical logic and type theory

lists the followings as the basic rules of simple type theory:

(1) identity

$\frac{}{x:X\vdash x:X}$

(2) function symbol

$\frac{M_1:x_1\;\;\dots \;\; M_n:x_n}{F(M_1,\dots,M_n:x_{n+1}}$

for $F:x_1,\dots,x_n\to x_{n+1}$ in $\Sigma$

(3) weakening

(4) contraction

(5) exchange

where we omitted the $\Gamma \vdash$ which we could prefix to every typing judgement.

From these rule one can derive a further important rule:

(6) substitution

$\frac{x_n:s\vdash M:t\;\;\; N:s}{M[N/x_n]:t}$

Revision on February 26, 2013 at 01:17:22 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.