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

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

(2) function symbol

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

for F:x 1,,x nx n+1F: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

x n:sM:tN:sM[N/x n]:t\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.