rules of type theories (Rev #1, changes)

Showing changes from revision #0 to #1:
Added | ~~Removed~~ | ~~Chan~~ged

- 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}$